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