Anne is green. Anne is red. Anne is smart. Anne is white. Erin is cold. Erin is green. Erin is quiet. Erin is red. Erin is young. Fiona is red. Fiona is smart. Fiona is white. Fiona is young. Gary is cold. Gary is quiet. Smart, quiet things are white. If something is white then it is red. Quiet things are smart. White, red things are smart. All green things are white. If something is quiet and smart then it is young.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Smart, quiet things are white.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
White, red things are smart.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is quiet and smart then it is young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Anne is red.
True
1
proof
[(triple2 OR ((triple4) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("Anne" "is" "red" "+")
triple2
((triple4) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Fiona is not young.
False
1
inv-proof
[(triple13)]
("Fiona" "is" "young" "-")
triple13
Erin is smart.
True
2
proof
[(((triple7) -> rule3) OR ((((triple6) -> rule5) triple8) -> rule4) OR ((((triple6) -> rule5) ((((triple6) -> rule5)) -> rule2)) -> rule4))]
("Erin" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple6) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple6) -> (rule5 % int3)) ((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Gary is not smart.
False
2
inv-proof
[(((triple15) -> rule3))]
("Gary" "is" "smart" "-")
((triple15) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
True
4
proof
[(((triple15 ((triple15) -> rule3)) -> rule6))]
("Gary" "is" "young" "+")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not young.
False
4
inv-proof
[(((triple15 ((triple15) -> rule3)) -> rule6))]
("Gary" "is" "young" "-")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
True
5
proof
[(((((((triple15) -> rule3) triple15) -> rule1)) -> rule2))]
("Gary" "is" "red" "+")
((((((triple15) -> (rule3 % int3)) triple15) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not red.
False
5
inv-proof
[(((((((triple15) -> rule3) triple15) -> rule1)) -> rule2))]
("Gary" "is" "red" "-")
((((((triple15) -> (rule3 % int3)) triple15) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2 OR ((triple4) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] Anne is smart.[(triple3 OR ((triple4 triple2) -> rule4) OR ((triple4 ((triple4) -> rule2)) -> rule4) OR ((((triple1) -> rule5) triple2) -> rule4) OR ((((triple1) -> rule5) ((triple4) -> rule2)) -> rule4) OR ((triple4 ((((triple1) -> rule5)) -> rule2)) -> rule4) OR ((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule2)) -> rule4))] Anne is white.[(triple4 OR ((triple1) -> rule5))] Erin is cold.[(triple5)] Erin is green.[(triple6)] Erin is quiet.[(triple7)] Erin is red.[(triple8 OR ((((triple6) -> rule5)) -> rule2) OR ((((((triple7) -> rule3) triple7) -> rule1)) -> rule2))] Erin is young.[(triple9 OR ((triple7 ((triple7) -> rule3)) -> rule6) OR ((triple7 ((((triple6) -> rule5) triple8) -> rule4)) -> rule6) OR ((triple7 ((((triple6) -> rule5) ((((triple6) -> rule5)) -> rule2)) -> rule4)) -> rule6))] Fiona is red.[(triple10 OR ((triple12) -> rule2))] Fiona is smart.[(triple11 OR ((triple12 triple10) -> rule4) OR ((triple12 ((triple12) -> rule2)) -> rule4))] Fiona is white.[(triple12)] Fiona is young.[(triple13)] Gary is cold.[(triple14)] Gary is quiet.[(triple15)] @1: Erin is smart.[(((triple7) -> rule3) OR ((((triple6) -> rule5) triple8) -> rule4) OR ((((triple6) -> rule5) ((((triple6) -> rule5)) -> rule2)) -> rule4))] Erin is white.[(((triple6) -> rule5) OR ((((triple7) -> rule3) triple7) -> rule1))] Gary is smart.[(((triple15) -> rule3))] @2: Gary is white.[(((((triple15) -> rule3) triple15) -> rule1))] Gary is young.[(((triple15 ((triple15) -> rule3)) -> rule6))] @3: Gary is red.[(((((((triple15) -> rule3) triple15) -> rule1)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple4) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple4 triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple1) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((triple4 ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple9
((triple7 ((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((triple7 ((((triple6) -> (rule5 % int3)) triple8) -> (rule4 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((triple7 ((((triple6) -> (rule5 % int4)) ((((triple6) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
triple10
((triple12) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple12 triple10) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple12 ((triple12) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Fiona is young.
("Fiona" "is" "young" "+")
triple13
Gary is cold.
("Gary" "is" "cold" "+")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple6) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple6) -> (rule5 % int3)) ((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple15) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple15) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple15 ((triple15) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((((triple15) -> (rule3 % int3)) triple15) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3