Anne is blue. Anne is cold. Anne is not kind. Anne is red. Anne is smart. Anne is young. Bob is quiet. Erin is cold. Erin is kind. Erin is red. Erin is young. Gary is kind. If someone is kind then they are cold. All cold people are smart. If Erin is smart and Erin is not cold then Erin is blue. All red people are quiet. All quiet people are blue. All smart people are red. If someone is quiet and not smart then they are not red. All young people are red.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Erin is smart and Erin is not cold then Erin is blue.
((("Erin" "is" "smart" "+") ("Erin" "is" "cold" "~")) -> ("Erin" "is" "blue" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet and not smart then they are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "red" "-"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Anne is not kind.
True
1
proof
[(triple3)]
("Anne" "is" "kind" "-")
triple3
Erin is not young.
False
1
inv-proof
[(triple11)]
("Erin" "is" "young" "-")
triple11
Gary is cold.
True
2
proof
[(((triple12) -> rule1))]
("Gary" "is" "cold" "+")
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple7) -> rule5))]
("Bob" "is" "blue" "-")
((triple7) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is blue.
True
3
proof
[(((((triple10) -> rule4)) -> rule5) OR ((((((triple11) -> rule8)) -> rule4)) -> rule5) OR ((((((((triple8) -> rule2)) -> rule6)) -> rule4)) -> rule5) OR ((((((((((triple9) -> rule1)) -> rule2)) -> rule6)) -> rule4)) -> rule5))]
("Erin" "is" "blue" "+")
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((((triple8) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((((((triple9) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Gary is not smart.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2))]
("Gary" "is" "smart" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
True
4
proof
[(((((((triple12) -> rule1)) -> rule2)) -> rule6))]
("Gary" "is" "red" "+")
((((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not red.
False
4
inv-proof
[(((((((triple12) -> rule1)) -> rule2)) -> rule6))]
("Gary" "is" "red" "-")
((((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
True
5
proof
[(((((((((triple12) -> rule1)) -> rule2)) -> rule6)) -> rule4))]
("Gary" "is" "quiet" "+")
((((((((triple12) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is not quiet.
False
5
inv-proof
[(((((((((triple12) -> rule1)) -> rule2)) -> rule6)) -> rule4))]
("Gary" "is" "quiet" "-")
((((((((triple12) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is blue.
True
6
proof
[(((((((((((triple12) -> rule1)) -> rule2)) -> rule6)) -> rule4)) -> rule5))]
("Gary" "is" "blue" "+")
((((((((((triple12) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5
Gary is not blue.
False
6
inv-proof
[(((((((((((triple12) -> rule1)) -> rule2)) -> rule6)) -> rule4)) -> rule5))]
("Gary" "is" "blue" "-")
((((((((((triple12) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is red.
Unknown
rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is blue.[(triple1 OR ((((triple4) -> rule4)) -> rule5) OR ((((((triple5) -> rule6)) -> rule4)) -> rule5) OR ((((((triple6) -> rule8)) -> rule4)) -> rule5) OR ((((((((triple2) -> rule2)) -> rule6)) -> rule4)) -> rule5))] Anne is cold.[(triple2)] Anne is not kind.[(triple3)] Anne is red.[(triple4 OR ((triple5) -> rule6) OR ((triple6) -> rule8) OR ((((triple2) -> rule2)) -> rule6))] Anne is smart.[(triple5 OR ((triple2) -> rule2))] Anne is young.[(triple6)] Bob is quiet.[(triple7)] Erin is cold.[(triple8 OR ((triple9) -> rule1))] Erin is kind.[(triple9)] Erin is red.[(triple10 OR ((triple11) -> rule8) OR ((((triple8) -> rule2)) -> rule6) OR ((((((triple9) -> rule1)) -> rule2)) -> rule6))] Erin is young.[(triple11)] Gary is kind.[(triple12)] @1: Anne is quiet.[(((triple4) -> rule4) OR ((((triple5) -> rule6)) -> rule4) OR ((((triple6) -> rule8)) -> rule4) OR ((((((triple2) -> rule2)) -> rule6)) -> rule4))] Bob is blue.[(((triple7) -> rule5))] Erin is quiet.[(((triple10) -> rule4) OR ((((triple11) -> rule8)) -> rule4) OR ((((((triple8) -> rule2)) -> rule6)) -> rule4) OR ((((((((triple9) -> rule1)) -> rule2)) -> rule6)) -> rule4))] Erin is smart.[(((triple8) -> rule2) OR ((((triple9) -> rule1)) -> rule2))] Gary is cold.[(((triple12) -> rule1))] @2: Erin is blue.[(((((triple10) -> rule4)) -> rule5) OR ((((((triple11) -> rule8)) -> rule4)) -> rule5) OR ((((((((triple8) -> rule2)) -> rule6)) -> rule4)) -> rule5) OR ((((((((((triple9) -> rule1)) -> rule2)) -> rule6)) -> rule4)) -> rule5))] Gary is smart.[(((((triple12) -> rule1)) -> rule2))] @3: Gary is red.[(((((((triple12) -> rule1)) -> rule2)) -> rule6))] @4: Gary is quiet.[(((((((((triple12) -> rule1)) -> rule2)) -> rule6)) -> rule4))] @5: Gary is blue.[(((((((((((triple12) -> rule1)) -> rule2)) -> rule6)) -> rule4)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((((triple6) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not kind.
("Anne" "is" "kind" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple5) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple6) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple9) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple10
((triple11) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple10) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((((triple9) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((((triple8) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((((((triple9) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Gary is smart.
("Gary" "is" "smart" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((((triple12) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
((((((((((triple12) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5