Anne is big. Anne is furry. Bob is big. Bob is young. Charlie is big. Harry is quiet. Harry is young. Young things are furry. Quiet, blue things are furry. If something is blue and furry then it is young. Young, quiet things are cold. If Bob is young and Bob is blue then Bob is round. All furry, big things are blue. If something is round then it is quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Quiet, blue things are furry.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is blue and furry then it is young.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Young, quiet things are cold.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Bob is young and Bob is blue then Bob is round.
((("Bob" "is" "young" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "+"))
All furry, big things are blue.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
Bob is furry.
True
2
proof
[(((triple4) -> rule1))]
("Bob" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is not blue.
False
3
inv-proof
[(((triple2 triple1) -> rule6))]
("Anne" "is" "blue" "-")
((triple2 triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is blue.
True
4
proof
[(((((triple4) -> rule1) triple3) -> rule6))]
("Bob" "is" "blue" "+")
((((triple4) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((((triple4) -> rule1) triple3) -> rule6))]
("Bob" "is" "blue" "-")
((((triple4) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
True
6
proof
[(((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5))]
("Bob" "is" "round" "+")
((triple4 ((((triple4) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not round.
False
6
inv-proof
[(((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5))]
("Bob" "is" "round" "-")
((triple4 ((((triple4) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
True
7
proof
[(((((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5)) -> rule7))]
("Bob" "is" "quiet" "+")
((((triple4 ((((triple4) -> (rule1 % int4)) triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is not quiet.
False
7
inv-proof
[(((((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5)) -> rule7))]
("Bob" "is" "quiet" "-")
((((triple4 ((((triple4) -> (rule1 % int4)) triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is cold.
True
9
proof
[(((triple4 ((((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5)) -> rule7)) -> rule4))]
("Bob" "is" "cold" "+")
((triple4 ((((triple4 ((((triple4) -> (rule1 % int5)) triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
Bob is not cold.
False
9
inv-proof
[(((triple4 ((((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5)) -> rule7)) -> rule4))]
("Bob" "is" "cold" "-")
((triple4 ((((triple4 ((((triple4) -> (rule1 % int5)) triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5
Charlie is not furry.
Unknown
inv-rconc
[@4: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is young.
Unknown
rconc
[@3: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is cold.
Unknown
rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Bob is big.[(triple3)] Bob is young.[(triple4)] Charlie is big.[(triple5)] Harry is quiet.[(triple6)] Harry is young.[(triple7)] @1: Anne is blue.[(((triple2 triple1) -> rule6))] Bob is furry.[(((triple4) -> rule1))] Harry is cold.[(((triple7 triple6) -> rule4))] Harry is furry.[(((triple7) -> rule1))] @2: Anne is young.[(((((triple2 triple1) -> rule6) triple2) -> rule3))] Bob is blue.[(((((triple4) -> rule1) triple3) -> rule6))] @3: Bob is round.[(((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5))] @4: Bob is quiet.[(((((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5)) -> rule7))] @5: Bob is cold.[(((triple4 ((((triple4 ((((triple4) -> rule1) triple3) -> rule6)) -> rule5)) -> rule7)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 triple6) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2 triple1) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple4) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple4 ((((triple4) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple4 ((((triple4) -> (rule1 % int4)) triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((triple4 ((((triple4 ((((triple4) -> (rule1 % int5)) triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
int5