Anne is green. Anne is red. Anne is white. Bob is green. Bob is quiet. Bob is white. Charlie is green. Charlie is red. Dave is big. Dave is quiet. If someone is red then they are quiet. If Charlie is white and Charlie is rough then Charlie is green. All red, quiet people are white. If someone is rough and red then they are white. All red people are quiet. If Charlie is rough and Charlie is cold then Charlie is red. All big people are rough. If Bob is quiet then Bob is red.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is white and Charlie is rough then Charlie is green.
((("Charlie" "is" "white" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "green" "+"))
All red, quiet people are white.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is rough and red then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is rough and Charlie is cold then Charlie is red.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "red" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Bob is quiet then Bob is red.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "+"))
Charlie is green.
True
1
proof
[(triple7)]
("Charlie" "is" "green" "+")
triple7
Dave is not big.
False
1
inv-proof
[(triple9)]
("Dave" "is" "big" "-")
triple9
Dave is rough.
True
2
proof
[(((triple9) -> rule7))]
("Dave" "is" "rough" "+")
((triple9) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple9) -> rule7))]
("Dave" "is" "rough" "-")
((triple9) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is white.
True
4
proof
[(((triple8 ((triple8) -> rule1)) -> rule3) OR ((triple8 ((triple8) -> rule5)) -> rule3))]
("Charlie" "is" "white" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple8 ((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((triple8 ((triple8) -> rule1)) -> rule3) OR ((triple8 ((triple8) -> rule5)) -> rule3))]
("Charlie" "is" "white" "-")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple8 ((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2)] Anne is white.[(triple3 OR ((triple2 ((triple2) -> rule1)) -> rule3) OR ((triple2 ((triple2) -> rule5)) -> rule3))] Bob is green.[(triple4)] Bob is quiet.[(triple5)] Bob is white.[(triple6 OR ((((triple5) -> rule8) triple5) -> rule3))] Charlie is green.[(triple7)] Charlie is red.[(triple8)] Dave is big.[(triple9)] Dave is quiet.[(triple10)] @1: Anne is quiet.[(((triple2) -> rule1) OR ((triple2) -> rule5))] Bob is red.[(((triple5) -> rule8))] Charlie is quiet.[(((triple8) -> rule1) OR ((triple8) -> rule5))] Dave is rough.[(((triple9) -> rule7))] @2: Charlie is white.[(((triple8 ((triple8) -> rule1)) -> rule3) OR ((triple8 ((triple8) -> rule5)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((((triple5) -> (rule8 % int2)) triple5) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple5) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple8) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple8) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple9) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple8 ((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2