Anne is big. Anne is blue. Anne is kind. Anne is nice. Anne is red. Anne is young. Charlie is nice. Charlie is red. Dave is big. Dave is blue. Dave is cold. Dave is nice. Dave is red. Harry is blue. Harry is young. All red, cold people are blue. If someone is nice and young then they are big. If someone is nice and young then they are cold. Kind, big people are red. All blue people are young. If someone is big and cold then they are blue. All nice, cold people are red. Kind people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
All red, cold people are blue.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and young then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and young then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Kind, big people are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is big and cold then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All nice, cold people are red.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple3) -> rule8) OR ((triple4 triple6) -> rule2) OR ((triple4 ((triple2) -> rule5)) -> rule2))]
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple4 triple6) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple4 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not kind.
False
1
inv-proof
[(triple3)]
("Anne" "is" "kind" "-")
triple3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule8) OR ((triple4 triple6) -> rule2) OR ((triple4 ((triple2) -> rule5)) -> rule2))] Anne is blue.[(triple2 OR ((triple1 ((triple4 triple6) -> rule3)) -> rule6) OR ((triple5 ((triple4 triple6) -> rule3)) -> rule1) OR ((((triple3) -> rule8) ((triple4 triple6) -> rule3)) -> rule6) OR ((((triple3 triple1) -> rule4) ((triple4 triple6) -> rule3)) -> rule1) OR ((((triple4 triple6) -> rule2) ((triple4 triple6) -> rule3)) -> rule6) OR ((((triple3 ((triple3) -> rule8)) -> rule4) ((triple4 triple6) -> rule3)) -> rule1) OR ((((triple3 ((triple4 triple6) -> rule2)) -> rule4) ((triple4 triple6) -> rule3)) -> rule1) OR ((((triple4 ((triple4 triple6) -> rule3)) -> rule7) ((triple4 triple6) -> rule3)) -> rule1))] Anne is kind.[(triple3)] Anne is nice.[(triple4)] Anne is red.[(triple5 OR ((triple3 triple1) -> rule4) OR ((triple3 ((triple3) -> rule8)) -> rule4) OR ((triple3 ((triple4 triple6) -> rule2)) -> rule4) OR ((triple4 ((triple4 triple6) -> rule3)) -> rule7) OR ((triple3 ((triple4 ((triple2) -> rule5)) -> rule2)) -> rule4) OR ((triple4 ((triple4 ((triple2) -> rule5)) -> rule3)) -> rule7))] Anne is young.[(triple6 OR ((triple2) -> rule5))] Charlie is nice.[(triple7)] Charlie is red.[(triple8)] Dave is big.[(triple9 OR ((triple12 ((triple10) -> rule5)) -> rule2) OR ((triple12 ((((triple13 triple11) -> rule1)) -> rule5)) -> rule2) OR ((triple12 ((((((triple12 triple11) -> rule7) triple11) -> rule1)) -> rule5)) -> rule2))] Dave is blue.[(triple10 OR ((triple13 triple11) -> rule1) OR ((triple9 triple11) -> rule6) OR ((((triple12 triple11) -> rule7) triple11) -> rule1))] Dave is cold.[(triple11 OR ((triple12 ((triple10) -> rule5)) -> rule3))] Dave is nice.[(triple12)] Dave is red.[(triple13 OR ((triple12 triple11) -> rule7) OR ((triple12 ((triple12 ((triple10) -> rule5)) -> rule3)) -> rule7))] Harry is blue.[(triple14)] Harry is young.[(triple15 OR ((triple14) -> rule5))] @1: Anne is cold.[(((triple4 triple6) -> rule3) OR ((triple4 ((triple2) -> rule5)) -> rule3))] Dave is young.[(((triple10) -> rule5) OR ((((triple13 triple11) -> rule1)) -> rule5) OR ((((triple9 triple11) -> rule6)) -> rule5) OR ((((((triple12 triple11) -> rule7) triple11) -> rule1)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple4 triple6) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple4 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple1 ((triple4 triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple3) -> (rule8 % int3)) ((triple4 triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((triple3 triple1) -> (rule4 % int3)) ((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((triple4 triple6) -> (rule2 % int3)) ((triple4 triple6) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((triple3 ((triple3) -> (rule8 % int4))) -> (rule4 % int3)) ((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((triple3 ((triple4 triple6) -> (rule2 % int4))) -> (rule4 % int3)) ((triple4 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((triple4 ((triple4 triple6) -> (rule3 % int3))) -> (rule7 % int2)) ((triple4 triple6) -> (rule3 % int3))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple3 triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 ((triple3) -> (rule8 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple3 ((triple4 triple6) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple4 ((triple4 triple6) -> (rule3 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple3 ((triple4 ((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((triple4 ((triple4 ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple9
((triple12 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple12 ((((triple13 triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((triple12 ((((((triple12 triple11) -> (rule7 % int4)) triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
triple10
((triple13 triple11) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple9 triple11) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple12 triple11) -> (rule7 % int2)) triple11) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple11
((triple12 ((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
triple13
((triple12 triple11) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple12 ((triple12 ((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple14) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple4 triple6) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple4 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple10) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple13 triple11) -> (rule1 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple9 triple11) -> (rule6 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple12 triple11) -> (rule7 % int3)) triple11) -> (rule1 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3