Anne is rough. Bob is blue. Bob is cold. Charlie is quiet. Charlie is not rough. Charlie is white. Gary is blue. If something is blue then it is quiet. All quiet, blue things are green. Cold, green things are not white. If Anne is green then Anne is not cold. All green things are cold. If something is quiet and not white then it is not rough.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All quiet, blue things are green.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Cold, green things are not white.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "-"))
If Anne is green then Anne is not cold.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "-"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is quiet and not white then it is not rough.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "rough" "-"))
Gary is blue.
True
1
proof
[(triple7)]
("Gary" "is" "blue" "+")
triple7
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Bob" "is" "green" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not green.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("Bob" "is" "green" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not white.
True
6
proof
[(((triple3 ((((triple2) -> rule1) triple2) -> rule2)) -> rule3) OR ((((((((triple2) -> rule1) triple2) -> rule2)) -> rule5) ((((triple2) -> rule1) triple2) -> rule2)) -> rule3))]
("Bob" "is" "white" "-")
((triple3 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple2) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Gary is not cold.
False
5
inv-proof
[(((((((triple7) -> rule1) triple7) -> rule2)) -> rule5))]
("Gary" "is" "cold" "-")
((((((triple7) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not white.
True
10
proof
[(((((((((triple7) -> rule1) triple7) -> rule2)) -> rule5) ((((triple7) -> rule1) triple7) -> rule2)) -> rule3))]
("Gary" "is" "white" "-")
((((((((triple7) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Bob is rough.
False
9
inv-proof
[(((((triple2) -> rule1) ((triple3 ((((triple2) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6) OR ((((triple2) -> rule1) ((((((((triple2) -> rule1) triple2) -> rule2)) -> rule5) ((((triple2) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int4)) ((triple3 ((((triple2) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((triple2) -> (rule1 % int5)) ((((((((triple2) -> (rule1 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule1 % int5)) triple2) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Gary is not rough.
True
13
proof
[(((((triple7) -> rule1) ((((((((triple7) -> rule1) triple7) -> rule2)) -> rule5) ((((triple7) -> rule1) triple7) -> rule2)) -> rule3)) -> rule6))]
("Gary" "is" "rough" "-")
((((triple7) -> (rule1 % int5)) ((((((((triple7) -> (rule1 % int5)) triple7) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple7) -> (rule1 % int5)) triple7) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Gary is rough.
False
13
inv-proof
[(((((triple7) -> rule1) ((((((((triple7) -> rule1) triple7) -> rule2)) -> rule5) ((((triple7) -> rule1) triple7) -> rule2)) -> rule3)) -> rule6))]
("Gary" "is" "rough" "+")
((((triple7) -> (rule1 % int5)) ((((((((triple7) -> (rule1 % int5)) triple7) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple7) -> (rule1 % int5)) triple7) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is rough.[(triple1)] Bob is blue.[(triple2)] Bob is cold.[(triple3 OR ((((((triple2) -> rule1) triple2) -> rule2)) -> rule5))] Charlie is not rough.[(triple5)] Charlie is quiet.[(triple4)] Charlie is white.[(triple6)] Gary is blue.[(triple7)] @1: Bob is quiet.[(((triple2) -> rule1))] Gary is quiet.[(((triple7) -> rule1))] @2: Bob is green.[(((((triple2) -> rule1) triple2) -> rule2))] Gary is green.[(((((triple7) -> rule1) triple7) -> rule2))] @3: Bob is not white.[(((triple3 ((((triple2) -> rule1) triple2) -> rule2)) -> rule3) OR ((((((((triple2) -> rule1) triple2) -> rule2)) -> rule5) ((((triple2) -> rule1) triple2) -> rule2)) -> rule3))] Gary is cold.[(((((((triple7) -> rule1) triple7) -> rule2)) -> rule5))] @4: Bob is not rough.[(((((triple2) -> rule1) ((triple3 ((((triple2) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6) OR ((((triple2) -> rule1) ((((((((triple2) -> rule1) triple2) -> rule2)) -> rule5) ((((triple2) -> rule1) triple2) -> rule2)) -> rule3)) -> rule6))] Gary is not white.[(((((((((triple7) -> rule1) triple7) -> rule2)) -> rule5) ((((triple7) -> rule1) triple7) -> rule2)) -> rule3))] @5: Gary is not rough.[(((((triple7) -> rule1) ((((((((triple7) -> rule1) triple7) -> rule2)) -> rule5) ((((triple7) -> rule1) triple7) -> rule2)) -> rule3)) -> rule6))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple7) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
((triple3 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple2) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple2) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple7) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is not rough.
("Bob" "is" "rough" "-")
((((triple2) -> (rule1 % int4)) ((triple3 ((((triple2) -> (rule1 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((triple2) -> (rule1 % int5)) ((((((((triple2) -> (rule1 % int5)) triple2) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule1 % int5)) triple2) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Gary is not white.
("Gary" "is" "white" "-")
((((((((triple7) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple7) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is not rough.
("Gary" "is" "rough" "-")
((((triple7) -> (rule1 % int5)) ((((((((triple7) -> (rule1 % int5)) triple7) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple7) -> (rule1 % int5)) triple7) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5