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