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