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