Anne is round. Charlie is green. Charlie is white. Dave is blue. Dave is white. Gary is rough. Gary is round. If Anne is round then Anne is furry. Green people are rough. All round, blue people are rough. If someone is blue then they are white. Rough people are blue. If Dave is rough then Dave is blue. Rough people are green. Big people are white.
Anne is round.
("Anne" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If Anne is round then Anne is furry.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "furry" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All round, blue people are rough.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If Dave is rough then Dave is blue.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple7)]
("Gary" "is" "round" "-")
triple7
Charlie is rough.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple6) -> rule5))]
("Gary" "is" "blue" "-")
((triple6) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("Charlie" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4))]
("Gary" "is" "white" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@4: Anne is green.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is white.
Unknown
rconc
[@5: Anne is white.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule2 <- rule7 <- rule3 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not blue.
Unknown
inv-rconc
[@4: Anne is blue.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule7 <- rule3 <- FAIL)]]
("Anne" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is round.[(triple1)] Charlie is green.[(triple2)] Charlie is white.[(triple3 OR ((((((triple2) -> rule2)) -> rule5)) -> rule4))] Dave is blue.[(triple4)] Dave is white.[(triple5 OR ((triple4) -> rule4))] Gary is rough.[(triple6)] Gary is round.[(triple7)] @1: Anne is furry.[(((triple1) -> rule1))] Charlie is rough.[(((triple2) -> rule2))] Gary is blue.[(((triple6) -> rule5))] Gary is green.[(((triple6) -> rule7))] @2: Charlie is blue.[(((((triple2) -> rule2)) -> rule5))] Gary is white.[(((((triple6) -> rule5)) -> rule4))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple4) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple6) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2