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