Anne is furry. Charlie is big. Charlie is round. Charlie is smart. Dave is red. Harry is big. Harry is smart. Big things are blue. Furry things are smart. If something is round and big then it is smart. If something is round then it is cold. All cold things are blue. All cold, red things are big. If Charlie is big and Charlie is furry then Charlie is blue. Furry things are round.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is round and big then it is smart.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All cold, red things are big.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Charlie is big and Charlie is furry then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "blue" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Harry is smart.
True
1
proof
[(triple7)]
("Harry" "is" "smart" "+")
triple7
Dave is not red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "-")
triple5
Anne is smart.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule5))]
("Anne" "is" "blue" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not blue.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule5))]
("Anne" "is" "blue" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "round" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "big" "+")
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
rconc
[@4: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule4 <- rule8 <- FAIL)]]
("Dave" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Charlie is big.[(triple2)] Charlie is round.[(triple3)] Charlie is smart.[(triple4 OR ((triple3 triple2) -> rule3))] Dave is red.[(triple5)] Harry is big.[(triple6)] Harry is smart.[(triple7)] @1: Anne is round.[(((triple1) -> rule8))] Anne is smart.[(((triple1) -> rule2))] Charlie is blue.[(((triple2) -> rule1) OR ((((triple3) -> rule4)) -> rule5))] Charlie is cold.[(((triple3) -> rule4))] Harry is blue.[(((triple6) -> rule1))] @2: Anne is cold.[(((((triple1) -> rule8)) -> rule4))] @3: Anne is blue.[(((((((triple1) -> rule8)) -> rule4)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple3 triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3