Bob is big. Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Charlie is blue. Charlie is furry. Charlie is nice. Charlie is quiet. Gary is big. Gary is blue. Gary is cold. Gary is furry. Gary is green. Gary is nice. Gary is quiet. If something is big and furry then it is cold. Blue, quiet things are big. All furry, big things are cold. All blue, cold things are green. Cold things are furry. If Gary is green then Gary is nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is big and furry then it is cold.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Blue, quiet things are big.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
All furry, big things are cold.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All blue, cold things are green.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If Gary is green then Gary is nice.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "nice" "+"))
Charlie is quiet.
True
1
proof
[(triple9)]
("Charlie" "is" "quiet" "+")
triple9
Gary is not blue.
False
1
inv-proof
[(triple11)]
("Gary" "is" "blue" "-")
triple11
Charlie is big.
True
3
proof
[(((triple6 triple9) -> rule2))]
("Charlie" "is" "big" "+")
((triple6 triple9) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
3
inv-proof
[(((triple6 triple9) -> rule2))]
("Charlie" "is" "big" "-")
((triple6 triple9) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
True
5
proof
[(((triple7 ((triple6 triple9) -> rule2)) -> rule3) OR ((((triple6 triple9) -> rule2) triple7) -> rule1))]
("Charlie" "is" "cold" "+")
((triple7 ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple6 triple9) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not cold.
False
5
inv-proof
[(((triple7 ((triple6 triple9) -> rule2)) -> rule3) OR ((((triple6 triple9) -> rule2) triple7) -> rule1))]
("Charlie" "is" "cold" "-")
((triple7 ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple6 triple9) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
True
7
proof
[(((triple6 ((triple7 ((triple6 triple9) -> rule2)) -> rule3)) -> rule4) OR ((triple6 ((((triple6 triple9) -> rule2) triple7) -> rule1)) -> rule4))]
("Charlie" "is" "green" "+")
((triple6 ((triple7 ((triple6 triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple6 ((((triple6 triple9) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not green.
False
7
inv-proof
[(((triple6 ((triple7 ((triple6 triple9) -> rule2)) -> rule3)) -> rule4) OR ((triple6 ((((triple6 triple9) -> rule2) triple7) -> rule1)) -> rule4))]
("Charlie" "is" "green" "-")
((triple6 ((triple7 ((triple6 triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple6 ((((triple6 triple9) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple1 triple3) -> rule1) OR ((triple3 triple1) -> rule3))] Bob is furry.[(triple3 OR ((triple2) -> rule5))] Bob is nice.[(triple4)] Bob is quiet.[(triple5)] Charlie is blue.[(triple6)] Charlie is furry.[(triple7)] Charlie is nice.[(triple8)] Charlie is quiet.[(triple9)] Gary is big.[(triple10 OR ((triple11 triple16) -> rule2))] Gary is blue.[(triple11)] Gary is cold.[(triple12 OR ((triple10 triple13) -> rule1) OR ((triple13 triple10) -> rule3) OR ((triple13 ((triple11 triple16) -> rule2)) -> rule3) OR ((((triple11 triple16) -> rule2) triple13) -> rule1))] Gary is furry.[(triple13 OR ((triple12) -> rule5))] Gary is green.[(triple14 OR ((triple11 triple12) -> rule4) OR ((triple11 ((triple10 triple13) -> rule1)) -> rule4) OR ((triple11 ((triple13 triple10) -> rule3)) -> rule4) OR ((triple11 ((triple13 ((triple11 triple16) -> rule2)) -> rule3)) -> rule4) OR ((triple11 ((((triple11 triple16) -> rule2) triple13) -> rule1)) -> rule4))] Gary is nice.[(triple15 OR ((triple14) -> rule6) OR ((((triple11 triple12) -> rule4)) -> rule6) OR ((((triple11 ((triple10 triple13) -> rule1)) -> rule4)) -> rule6) OR ((((triple11 ((triple13 triple10) -> rule3)) -> rule4)) -> rule6) OR ((((triple11 ((triple13 ((triple11 triple16) -> rule2)) -> rule3)) -> rule4)) -> rule6) OR ((((triple11 ((((triple11 triple16) -> rule2) triple13) -> rule1)) -> rule4)) -> rule6))] Gary is quiet.[(triple16)] @1: Charlie is big.[(((triple6 triple9) -> rule2))] @2: Charlie is cold.[(((triple7 ((triple6 triple9) -> rule2)) -> rule3) OR ((((triple6 triple9) -> rule2) triple7) -> rule1))] @3: Charlie is green.[(((triple6 ((triple7 ((triple6 triple9) -> rule2)) -> rule3)) -> rule4) OR ((triple6 ((((triple6 triple9) -> rule2) triple7) -> rule1)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1 triple3) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple11 triple16) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((triple10 triple13) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple13 triple10) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple13 ((triple11 triple16) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple11 triple16) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple13
((triple12) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple14
((triple11 triple12) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple11 ((triple10 triple13) -> (rule1 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple11 ((triple13 triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple11 ((triple13 ((triple11 triple16) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple11 ((((triple11 triple16) -> (rule2 % int3)) triple13) -> (rule1 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple15
((triple14) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple11 triple12) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple11 ((triple10 triple13) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple11 ((triple13 triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple11 ((triple13 ((triple11 triple16) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((triple11 ((((triple11 triple16) -> (rule2 % int4)) triple13) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple16
Charlie is big.
("Charlie" "is" "big" "+")
((triple6 triple9) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple7 ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple6 triple9) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((triple6 ((triple7 ((triple6 triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple6 ((((triple6 triple9) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3