Anne is big. Anne is quiet. Anne is red. Anne is round. Bob is quiet. Bob is round. Bob is not white. Erin is big. Erin is quiet. Erin is red. Erin is round. Erin is white. Gary is blue. Gary is quiet. Gary is not round. Red, round things are big. If something is white then it is big. Round things are red. If something is red then it is not young. If something is blue and young then it is round. Red, round things are quiet. All young things are white. If something is red then it is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not white.
("Bob" "is" "white" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not round.
("Gary" "is" "round" "-")
Red, round things are big.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is red then it is not young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
If something is blue and young then it is round.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Red, round things are quiet.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Bob is round.
True
1
proof
[(triple6)]
("Bob" "is" "round" "+")
triple6
Bob is not quiet.
False
1
inv-proof
[(triple5 OR ((((triple6) -> rule3) triple6) -> rule6))]
("Bob" "is" "quiet" "-")
triple5
((((triple6) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
True
2
proof
[(((triple6) -> rule3))]
("Bob" "is" "red" "+")
((triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple10) -> rule8) OR ((((triple11) -> rule3)) -> rule8))]
("Erin" "is" "blue" "-")
((triple10) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Bob is blue.
True
3
proof
[(((((triple6) -> rule3)) -> rule8))]
("Bob" "is" "blue" "+")
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is young.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule4))]
("Bob" "is" "young" "+")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "white" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is big.[(triple1 OR ((triple3 triple4) -> rule1) OR ((((triple4) -> rule3) triple4) -> rule1))] Anne is quiet.[(triple2 OR ((triple3 triple4) -> rule6) OR ((((triple4) -> rule3) triple4) -> rule6))] Anne is red.[(triple3 OR ((triple4) -> rule3))] Anne is round.[(triple4)] Bob is not white.[(triple7)] Bob is quiet.[(triple5 OR ((((triple6) -> rule3) triple6) -> rule6))] Bob is round.[(triple6)] Erin is big.[(triple8 OR ((triple12) -> rule2) OR ((triple10 triple11) -> rule1) OR ((((triple11) -> rule3) triple11) -> rule1))] Erin is quiet.[(triple9 OR ((triple10 triple11) -> rule6) OR ((((triple11) -> rule3) triple11) -> rule6))] Erin is red.[(triple10 OR ((triple11) -> rule3))] Erin is round.[(triple11)] Erin is white.[(triple12)] Gary is blue.[(triple13)] Gary is not round.[(triple15)] Gary is quiet.[(triple14)] @1: Anne is blue.[(((triple3) -> rule8) OR ((((triple4) -> rule3)) -> rule8))] Anne is not young.[(((triple3) -> rule4) OR ((((triple4) -> rule3)) -> rule4))] Bob is red.[(((triple6) -> rule3))] Erin is blue.[(((triple10) -> rule8) OR ((((triple11) -> rule3)) -> rule8))] Erin is not young.[(((triple10) -> rule4) OR ((((triple11) -> rule3)) -> rule4))] @2: Bob is big.[(((((triple6) -> rule3) triple6) -> rule1))] Bob is blue.[(((((triple6) -> rule3)) -> rule8))] Bob is not young.[(((((triple6) -> rule3)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3 triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3 triple4) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple4) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple4
Bob is not white.
("Bob" "is" "white" "-")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((((triple6) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple12) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple10 triple11) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple11) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple10 triple11) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple11) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple10
((triple11) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
triple13
Gary is not round.
("Gary" "is" "round" "-")
triple15
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not young.
("Anne" "is" "young" "-")
((triple3) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple10) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
((triple10) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
((((triple11) -> (rule3 % int2))) -> (rule4 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((triple6) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not young.
("Bob" "is" "young" "-")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
int2