Anne is big. Anne is cold. Anne is green. Anne is round. Bob is big. Bob is cold. Bob is round. Harry is blue. Harry is cold. Harry is quiet. If Bob is round and Bob is quiet then Bob is green. All big, cold people are quiet. All green people are big. If someone is green then they are blue. If Bob is quiet then Bob is round. All round people are cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Bob is round and Bob is quiet then Bob is green.
((("Bob" "is" "round" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "green" "+"))
All big, cold people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Bob is quiet then Bob is round.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "round" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple6 OR ((triple7) -> rule6))]
("Bob" "is" "cold" "+")
triple6
((triple7) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Harry is not blue.
False
1
inv-proof
[(triple8)]
("Harry" "is" "blue" "-")
triple8
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule3))] Anne is cold.[(triple2 OR ((triple4) -> rule6))] Anne is green.[(triple3)] Anne is round.[(triple4)] Bob is big.[(triple5)] Bob is cold.[(triple6 OR ((triple7) -> rule6))] Bob is round.[(triple7 OR ((((triple5 triple6) -> rule2)) -> rule5))] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is quiet.[(triple10)] @1: Anne is blue.[(((triple3) -> rule4))] Anne is quiet.[(((triple1 triple2) -> rule2) OR ((triple1 ((triple4) -> rule6)) -> rule2) OR ((((triple3) -> rule3) triple2) -> rule2) OR ((((triple3) -> rule3) ((triple4) -> rule6)) -> rule2))] Bob is quiet.[(((triple5 triple6) -> rule2) OR ((triple5 ((triple7) -> rule6)) -> rule2))] @2: Bob is green.[(((triple7 ((triple5 triple6) -> rule2)) -> rule1) OR ((triple7 ((triple5 ((triple7) -> rule6)) -> rule2)) -> rule1) OR ((((((triple5 triple6) -> rule2)) -> rule5) ((triple5 triple6) -> rule2)) -> rule1) OR ((((((triple5 triple6) -> rule2)) -> rule5) ((triple5 ((triple7) -> rule6)) -> rule2)) -> rule1))] @3: Bob is blue.[(((((triple7 ((triple5 triple6) -> rule2)) -> rule1)) -> rule4) OR ((((triple7 ((triple5 ((triple7) -> rule6)) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple5 triple6) -> rule2)) -> rule5) ((triple5 triple6) -> rule2)) -> rule1)) -> rule4) OR ((((((((triple5 triple6) -> rule2)) -> rule5) ((triple5 ((triple7) -> rule6)) -> rule2)) -> rule1)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is cold.
("Bob" "is" "cold" "+")
triple6
((triple7) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple7
((((triple5 triple6) -> (rule2 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple1 ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple5 triple6) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple5 ((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple7 ((triple5 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((triple7 ((triple5 ((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple5 triple6) -> (rule2 % int3))) -> (rule5 % int2)) ((triple5 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple5 triple6) -> (rule2 % int4))) -> (rule5 % int3)) ((triple5 ((triple7) -> (rule6 % int2))) -> (rule2 % int4))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
((((triple7 ((triple5 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((triple7 ((triple5 ((triple7) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((((((triple5 triple6) -> (rule2 % int4))) -> (rule5 % int3)) ((triple5 triple6) -> (rule2 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((((triple5 triple6) -> (rule2 % int5))) -> (rule5 % int4)) ((triple5 ((triple7) -> (rule6 % int3))) -> (rule2 % int5))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5