Charlie is big. Charlie is cold. Charlie is green. Charlie is rough. Charlie is smart. Charlie is white. Harry is big. Harry is green. Harry is round. Harry is white. If someone is cold and round then they are smart. If someone is big and green then they are cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is cold and round then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and green then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Harry is green.
True
1
proof
[(triple8)]
("Harry" "is" "green" "+")
triple8
Charlie is not rough.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "rough" "-")
triple4
Harry is cold.
True
3
proof
[(((triple7 triple8) -> rule2))]
("Harry" "is" "cold" "+")
((triple7 triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
3
inv-proof
[(((triple7 triple8) -> rule2))]
("Harry" "is" "cold" "-")
((triple7 triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
True
5
proof
[(((((triple7 triple8) -> rule2) triple9) -> rule1))]
("Harry" "is" "smart" "+")
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not smart.
False
5
inv-proof
[(((((triple7 triple8) -> rule2) triple9) -> rule1))]
("Harry" "is" "smart" "-")
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2 OR ((triple1 triple3) -> rule2))] Charlie is green.[(triple3)] Charlie is rough.[(triple4)] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Harry is big.[(triple7)] Harry is green.[(triple8)] Harry is round.[(triple9)] Harry is white.[(triple10)] @1: Harry is cold.[(((triple7 triple8) -> rule2))] @2: Harry is smart.[(((((triple7 triple8) -> rule2) triple9) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple1 triple3) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2