Anne is round. Anne is smart. Bob is blue. Bob is cold. Bob is furry. Bob is green. Charlie is cold. Charlie is green. Charlie is round. Charlie is smart. Gary is green. Gary is quiet. If something is quiet and furry then it is cold. If Bob is blue and Bob is green then Bob is smart. All round, blue things are furry. If Gary is green then Gary is smart. If Bob is round then Bob is smart. If something is cold then it is quiet. Smart things are blue. If something is round and blue then it is green. Blue, green things are round.
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is quiet and furry then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If Bob is blue and Bob is green then Bob is smart.
((("Bob" "is" "blue" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
All round, blue things are furry.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If Gary is green then Gary is smart.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "smart" "+"))
If Bob is round then Bob is smart.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "smart" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is round and blue then it is green.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Blue, green things are round.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Gary is green.
True
1
proof
[(triple11)]
("Gary" "is" "green" "+")
triple11
Bob is not furry.
False
1
inv-proof
[(triple5 OR ((((triple3 triple6) -> rule9) triple3) -> rule3))]
("Bob" "is" "furry" "-")
triple5
((((triple3 triple6) -> (rule9 % int2)) triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
True
3
proof
[(((triple3 triple6) -> rule2) OR ((((triple3 triple6) -> rule9)) -> rule5))]
("Bob" "is" "smart" "+")
((triple3 triple6) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3 triple6) -> (rule9 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is not quiet.
False
2
inv-proof
[(((triple7) -> rule6))]
("Charlie" "is" "quiet" "-")
((triple7) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is green.
True
4
proof
[(((triple1 ((triple2) -> rule7)) -> rule8))]
("Anne" "is" "green" "+")
((triple1 ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not furry.
False
4
inv-proof
[(((triple1 ((triple2) -> rule7)) -> rule3))]
("Anne" "is" "furry" "-")
((triple1 ((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Gary is round.
True
5
proof
[(((((((triple11) -> rule4)) -> rule7) triple11) -> rule9))]
("Gary" "is" "round" "+")
((((((triple11) -> (rule4 % int3))) -> (rule7 % int2)) triple11) -> (rule9 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not round.
False
5
inv-proof
[(((((((triple11) -> rule4)) -> rule7) triple11) -> rule9))]
("Gary" "is" "round" "-")
((((((triple11) -> (rule4 % int3))) -> (rule7 % int2)) triple11) -> (rule9 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is furry.
True
9
proof
[(((((((((triple11) -> rule4)) -> rule7) triple11) -> rule9) ((((triple11) -> rule4)) -> rule7)) -> rule3))]
("Gary" "is" "furry" "+")
((((((((triple11) -> (rule4 % int4))) -> (rule7 % int3)) triple11) -> (rule9 % int2)) ((((triple11) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not furry.
False
9
inv-proof
[(((((((((triple11) -> rule4)) -> rule7) triple11) -> rule9) ((((triple11) -> rule4)) -> rule7)) -> rule3))]
("Gary" "is" "furry" "-")
((((((((triple11) -> (rule4 % int4))) -> (rule7 % int3)) triple11) -> (rule9 % int2)) ((((triple11) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
True
11
proof
[(((triple12 ((((((((triple11) -> rule4)) -> rule7) triple11) -> rule9) ((((triple11) -> rule4)) -> rule7)) -> rule3)) -> rule1))]
("Gary" "is" "cold" "+")
((triple12 ((((((((triple11) -> (rule4 % int5))) -> (rule7 % int4)) triple11) -> (rule9 % int3)) ((((triple11) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is not cold.
False
11
inv-proof
[(((triple12 ((((((((triple11) -> rule4)) -> rule7) triple11) -> rule9) ((((triple11) -> rule4)) -> rule7)) -> rule3)) -> rule1))]
("Gary" "is" "cold" "-")
((triple12 ((((((((triple11) -> (rule4 % int5))) -> (rule7 % int4)) triple11) -> (rule9 % int3)) ((((triple11) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is round.[(triple1)] Anne is smart.[(triple2)] Bob is blue.[(triple3)] Bob is cold.[(triple4)] Bob is furry.[(triple5 OR ((((triple3 triple6) -> rule9) triple3) -> rule3))] Bob is green.[(triple6)] Charlie is cold.[(triple7)] Charlie is green.[(triple8 OR ((triple9 ((triple10) -> rule7)) -> rule8))] Charlie is round.[(triple9 OR ((((triple10) -> rule7) triple8) -> rule9))] Charlie is smart.[(triple10)] Gary is green.[(triple11)] Gary is quiet.[(triple12)] @1: Anne is blue.[(((triple2) -> rule7))] Bob is quiet.[(((triple4) -> rule6))] Bob is round.[(((triple3 triple6) -> rule9))] Bob is smart.[(((triple3 triple6) -> rule2) OR ((((triple3 triple6) -> rule9)) -> rule5))] Charlie is blue.[(((triple10) -> rule7))] Charlie is quiet.[(((triple7) -> rule6))] Gary is smart.[(((triple11) -> rule4))] @2: Anne is furry.[(((triple1 ((triple2) -> rule7)) -> rule3))] Anne is green.[(((triple1 ((triple2) -> rule7)) -> rule8))] Charlie is furry.[(((triple9 ((triple10) -> rule7)) -> rule3) OR ((((((triple10) -> rule7) triple8) -> rule9) ((triple10) -> rule7)) -> rule3))] Gary is blue.[(((((triple11) -> rule4)) -> rule7))] @3: Gary is round.[(((((((triple11) -> rule4)) -> rule7) triple11) -> rule9))] @4: Gary is furry.[(((((((((triple11) -> rule4)) -> rule7) triple11) -> rule9) ((((triple11) -> rule4)) -> rule7)) -> rule3))] @5: Gary is cold.[(((triple12 ((((((((triple11) -> rule4)) -> rule7) triple11) -> rule9) ((((triple11) -> rule4)) -> rule7)) -> rule3)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
((((triple3 triple6) -> (rule9 % int2)) triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple9 ((triple10) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple9
((((triple10) -> (rule7 % int2)) triple8) -> (rule9 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple6) -> (rule9 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple3 triple6) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3 triple6) -> (rule9 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple10) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple7) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple11) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple9 ((triple10) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple10) -> (rule7 % int3)) triple8) -> (rule9 % int2)) ((triple10) -> (rule7 % int3))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((triple11) -> (rule4 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((((triple11) -> (rule4 % int3))) -> (rule7 % int2)) triple11) -> (rule9 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((((triple11) -> (rule4 % int4))) -> (rule7 % int3)) triple11) -> (rule9 % int2)) ((((triple11) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((triple12 ((((((((triple11) -> (rule4 % int5))) -> (rule7 % int4)) triple11) -> (rule9 % int3)) ((((triple11) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5