Anne is big. Anne is cold. Anne is kind. Anne is red. Anne is rough. Bob is furry. Bob is young. Charlie is big. Charlie is cold. Charlie is kind. Erin is big. Erin is cold. Erin is furry. Erin is red. Erin is rough. Erin is young. If something is rough then it is cold. All young things are rough. All cold things are furry. All red, young things are cold. If Erin is furry then Erin is big. Big, kind things are red. If something is cold then it is young. Furry things are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All red, young things are cold.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If Erin is furry then Erin is big.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "big" "+"))
Big, kind things are red.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Charlie is big.
True
1
proof
[(triple8)]
("Charlie" "is" "big" "+")
triple8
Charlie is not big.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "big" "-")
triple8
Bob is rough.
True
2
proof
[(((triple7) -> rule2) OR ((((triple6) -> rule8)) -> rule2))]
("Bob" "is" "rough" "+")
((triple7) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((triple8 triple10) -> rule6))]
("Charlie" "is" "red" "-")
((triple8 triple10) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple5) -> rule1))] Anne is kind.[(triple3)] Anne is red.[(triple4 OR ((triple1 triple3) -> rule6))] Anne is rough.[(triple5 OR ((((triple2) -> rule7)) -> rule2) OR ((((((triple2) -> rule3)) -> rule8)) -> rule2))] Bob is furry.[(triple6 OR ((((((triple7) -> rule2)) -> rule1)) -> rule3))] Bob is young.[(triple7 OR ((triple6) -> rule8))] Charlie is big.[(triple8)] Charlie is cold.[(triple9)] Charlie is kind.[(triple10)] Erin is big.[(triple11 OR ((triple13) -> rule5) OR ((((triple12) -> rule3)) -> rule5) OR ((((((triple15) -> rule1)) -> rule3)) -> rule5) OR ((((((triple14 triple16) -> rule4)) -> rule3)) -> rule5) OR ((((((((triple16) -> rule2)) -> rule1)) -> rule3)) -> rule5))] Erin is cold.[(triple12 OR ((triple15) -> rule1) OR ((triple14 triple16) -> rule4) OR ((((triple16) -> rule2)) -> rule1) OR ((triple14 ((triple13) -> rule8)) -> rule4) OR ((((((triple13) -> rule8)) -> rule2)) -> rule1))] Erin is furry.[(triple13 OR ((triple12) -> rule3) OR ((((triple15) -> rule1)) -> rule3) OR ((((triple14 triple16) -> rule4)) -> rule3) OR ((((((triple16) -> rule2)) -> rule1)) -> rule3))] Erin is red.[(triple14)] Erin is rough.[(triple15 OR ((triple16) -> rule2) OR ((((triple12) -> rule7)) -> rule2) OR ((((triple13) -> rule8)) -> rule2) OR ((((((triple12) -> rule3)) -> rule8)) -> rule2))] Erin is young.[(triple16 OR ((triple12) -> rule7) OR ((triple13) -> rule8) OR ((((triple12) -> rule3)) -> rule8) OR ((((triple15) -> rule1)) -> rule7) OR ((((((triple15) -> rule1)) -> rule3)) -> rule8))] @1: Anne is furry.[(((triple2) -> rule3) OR ((((triple5) -> rule1)) -> rule3))] Anne is young.[(((triple2) -> rule7) OR ((((triple2) -> rule3)) -> rule8) OR ((((triple5) -> rule1)) -> rule7) OR ((((((triple5) -> rule1)) -> rule3)) -> rule8))] Bob is rough.[(((triple7) -> rule2) OR ((((triple6) -> rule8)) -> rule2))] Charlie is furry.[(((triple9) -> rule3))] Charlie is red.[(((triple8 triple10) -> rule6))] Charlie is young.[(((triple9) -> rule7) OR ((((triple9) -> rule3)) -> rule8))] @2: Bob is cold.[(((((triple7) -> rule2)) -> rule1) OR ((((((triple6) -> rule8)) -> rule2)) -> rule1))] Charlie is rough.[(((((triple9) -> rule7)) -> rule2) OR ((((((triple9) -> rule3)) -> rule8)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple5) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1 triple3) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple6
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple6) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((triple13) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple15) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple14 triple16) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple16) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
triple12
((triple15) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple14 triple16) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple16) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple14 ((triple13) -> (rule8 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple13) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple13
((triple12) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple14 triple16) -> (rule4 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple16) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
triple14
Erin is rough.
("Erin" "is" "rough" "+")
triple15
((triple16) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple12) -> (rule7 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple13) -> (rule8 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple12) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple16
((triple12) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple13) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple15) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple15) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((triple7) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple9) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple8 triple10) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple9) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple6) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple9) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple9) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3