Anne is green. Anne is white. Dave is not green. Dave is quiet. Dave is smart. Dave is white. Erin is smart. All quiet people are white. Quiet, round people are rough. If Anne is white and Anne is smart then Anne is rough. Smart, white people are round. If someone is smart and not white then they are round. Rough people are smart.
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Quiet, round people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If Anne is white and Anne is smart then Anne is rough.
((("Anne" "is" "white" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "rough" "+"))
Smart, white people are round.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and not white then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "round" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple7)]
("Erin" "is" "smart" "+")
triple7
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Dave is round.
True
3
proof
[(((triple5 triple6) -> rule4) OR ((triple5 ((triple4) -> rule1)) -> rule4))]
("Dave" "is" "round" "+")
((triple5 triple6) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple5 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not round.
False
3
inv-proof
[(((triple5 triple6) -> rule4) OR ((triple5 ((triple4) -> rule1)) -> rule4))]
("Dave" "is" "round" "-")
((triple5 triple6) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple5 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
True
5
proof
[(((triple4 ((triple5 triple6) -> rule4)) -> rule2) OR ((triple4 ((triple5 ((triple4) -> rule1)) -> rule4)) -> rule2))]
("Dave" "is" "rough" "+")
((triple4 ((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple4 ((triple5 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not rough.
False
5
inv-proof
[(((triple4 ((triple5 triple6) -> rule4)) -> rule2) OR ((triple4 ((triple5 ((triple4) -> rule1)) -> rule4)) -> rule2))]
("Dave" "is" "rough" "-")
((triple4 ((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple4 ((triple5 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "-")
Erin is round.
Unknown
rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is green.[(triple1)] Anne is white.[(triple2)] Dave is not green.[(triple3)] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Dave is white.[(triple6 OR ((triple4) -> rule1))] Erin is smart.[(triple7)] @1: Dave is round.[(((triple5 triple6) -> rule4) OR ((triple5 ((triple4) -> rule1)) -> rule4))] @2: Dave is rough.[(((triple4 ((triple5 triple6) -> rule4)) -> rule2) OR ((triple4 ((triple5 ((triple4) -> rule1)) -> rule4)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Dave is not green.
("Dave" "is" "green" "-")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple4) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
((triple5 triple6) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple5 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple4 ((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple4 ((triple5 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3