Anne is cold. Anne is green. Bob is quiet. Dave is furry. Dave is green. Dave is red. Gary is cold. All cold, rough things are furry. All green, red things are furry. Cold, red things are green. Cold things are quiet. Big, cold things are rough. If something is quiet then it is rough. If Bob is rough then Bob is furry. All furry, quiet things are red.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All cold, rough things are furry.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All green, red things are furry.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Cold, red things are green.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Big, cold things are rough.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If Bob is rough then Bob is furry.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "furry" "+"))
All furry, quiet things are red.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Dave is red.
True
1
proof
[(triple6)]
("Dave" "is" "red" "+")
triple6
Anne is not green.
False
1
inv-proof
[(triple2 OR ((triple1 ((((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule1) ((triple1) -> rule4)) -> rule8)) -> rule3))]
("Anne" "is" "green" "-")
triple2
((triple1 ((((triple1 ((((triple1) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1) -> (rule4 % int5))) -> (rule8 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Gary is quiet.
True
2
proof
[(((triple7) -> rule4))]
("Gary" "is" "quiet" "+")
((triple7) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Gary is rough.
True
3
proof
[(((((triple7) -> rule4)) -> rule6))]
("Gary" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule7))]
("Bob" "is" "furry" "-")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
True
5
proof
[(((((((triple3) -> rule6)) -> rule7) triple3) -> rule8))]
("Bob" "is" "red" "+")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2)) triple3) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Gary is not furry.
False
5
inv-proof
[(((triple7 ((((triple7) -> rule4)) -> rule6)) -> rule1))]
("Gary" "is" "furry" "-")
((triple7 ((((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "quiet" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2 OR ((triple1 ((((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule1) ((triple1) -> rule4)) -> rule8)) -> rule3))] Bob is quiet.[(triple3)] Dave is furry.[(triple4 OR ((triple5 triple6) -> rule2))] Dave is green.[(triple5)] Dave is red.[(triple6)] Gary is cold.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule4))] Bob is rough.[(((triple3) -> rule6))] Gary is quiet.[(((triple7) -> rule4))] @2: Anne is rough.[(((((triple1) -> rule4)) -> rule6))] Bob is furry.[(((((triple3) -> rule6)) -> rule7))] Gary is rough.[(((((triple7) -> rule4)) -> rule6))] @3: Anne is furry.[(((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule1))] Bob is red.[(((((((triple3) -> rule6)) -> rule7) triple3) -> rule8))] Gary is furry.[(((triple7 ((((triple7) -> rule4)) -> rule6)) -> rule1))] @4: Anne is red.[(((((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule1) ((triple1) -> rule4)) -> rule8))] Gary is red.[(((((triple7 ((((triple7) -> rule4)) -> rule6)) -> rule1) ((triple7) -> rule4)) -> rule8))] @5: Gary is green.[(((triple7 ((((triple7 ((((triple7) -> rule4)) -> rule6)) -> rule1) ((triple7) -> rule4)) -> rule8)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1 ((((triple1 ((((triple1) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple1) -> (rule4 % int5))) -> (rule8 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple5 triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2)) triple3) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((triple7 ((((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple1) -> (rule4 % int4))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
((((triple7 ((((triple7) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2)) ((triple7) -> (rule4 % int4))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
((triple7 ((((triple7 ((((triple7) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple7) -> (rule4 % int5))) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5