Charlie is big. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is red. Charlie is white. Charlie is young. Erin is big. Erin is cold. Erin is nice. Erin is red. Erin is white. Erin is young. Harry is big. Harry is red. Harry is young. All young things are cold. If something is big and cold then it is white. If something is cold then it is big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is big and cold then it is white.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple14 OR ((((triple16) -> rule1)) -> rule3))]
("Harry" "is" "big" "+")
triple14
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule3) OR ((((triple7) -> rule1)) -> rule3))]
("Charlie" "is" "big" "-")
triple1
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Harry is cold.
True
2
proof
[(((triple16) -> rule1))]
("Harry" "is" "cold" "+")
((triple16) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple16) -> rule1))]
("Harry" "is" "cold" "-")
((triple16) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
4
proof
[(((triple14 ((triple16) -> rule1)) -> rule2) OR ((((((triple16) -> rule1)) -> rule3) ((triple16) -> rule1)) -> rule2))]
("Harry" "is" "white" "+")
((triple14 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2)) ((triple16) -> (rule1 % int3))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not white.
False
4
inv-proof
[(((triple14 ((triple16) -> rule1)) -> rule2) OR ((((((triple16) -> rule1)) -> rule3) ((triple16) -> rule1)) -> rule2))]
("Harry" "is" "white" "-")
((triple14 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2)) ((triple16) -> (rule1 % int3))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Charlie is big.[(triple1 OR ((triple2) -> rule3) OR ((((triple7) -> rule1)) -> rule3))] Charlie is cold.[(triple2 OR ((triple7) -> rule1))] Charlie is furry.[(triple3)] Charlie is nice.[(triple4)] Charlie is red.[(triple5)] Charlie is white.[(triple6 OR ((triple1 triple2) -> rule2) OR ((triple1 ((triple7) -> rule1)) -> rule2) OR ((((triple2) -> rule3) triple2) -> rule2) OR ((((triple2) -> rule3) ((triple7) -> rule1)) -> rule2) OR ((((((triple7) -> rule1)) -> rule3) triple2) -> rule2) OR ((((((triple7) -> rule1)) -> rule3) ((triple7) -> rule1)) -> rule2))] Charlie is young.[(triple7)] Erin is big.[(triple8 OR ((triple9) -> rule3) OR ((((triple13) -> rule1)) -> rule3))] Erin is cold.[(triple9 OR ((triple13) -> rule1))] Erin is nice.[(triple10)] Erin is red.[(triple11)] Erin is white.[(triple12 OR ((triple8 triple9) -> rule2) OR ((triple8 ((triple13) -> rule1)) -> rule2) OR ((((triple9) -> rule3) triple9) -> rule2) OR ((((triple9) -> rule3) ((triple13) -> rule1)) -> rule2) OR ((((((triple13) -> rule1)) -> rule3) triple9) -> rule2) OR ((((((triple13) -> rule1)) -> rule3) ((triple13) -> rule1)) -> rule2))] Erin is young.[(triple13)] Harry is big.[(triple14 OR ((((triple16) -> rule1)) -> rule3))] Harry is red.[(triple15)] Harry is young.[(triple16)] @1: Harry is cold.[(((triple16) -> rule1))] @2: Harry is white.[(((triple14 ((triple16) -> rule1)) -> rule2) OR ((((((triple16) -> rule1)) -> rule3) ((triple16) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple1 triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple1 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple2) -> (rule3 % int3)) ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule3 % int2)) ((triple7) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple9) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple13) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple8 triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8 ((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple9) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((((triple13) -> (rule1 % int3))) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple13) -> (rule1 % int3))) -> (rule3 % int2)) ((triple13) -> (rule1 % int3))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
((((triple16) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Harry is cold.
("Harry" "is" "cold" "+")
((triple16) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple14 ((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule3 % int2)) ((triple16) -> (rule1 % int3))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3