Anne is blue. Bob is not blue. Bob is green. Bob is quiet. Erin is big. Erin is nice. Erin is rough. All green people are quiet. If Anne is not cold then Anne is rough. If Erin is rough then Erin is cold. Big, cold people are green. Blue people are rough. If Bob is blue and Bob is big then Bob is green.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is not cold then Anne is rough.
((("Anne" "is" "cold" "~")) -> ("Anne" "is" "rough" "+"))
If Erin is rough then Erin is cold.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "cold" "+"))
Big, cold people are green.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Bob is blue and Bob is big then Bob is green.
((("Bob" "is" "blue" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "green" "+"))
Erin is big.
True
1
proof
[(triple5)]
("Erin" "is" "big" "+")
triple5
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Erin is cold.
True
2
proof
[(((triple7) -> rule3))]
("Erin" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple7) -> rule3))]
("Erin" "is" "cold" "-")
((triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
True
4
proof
[(((triple5 ((triple7) -> rule3)) -> rule4))]
("Erin" "is" "green" "+")
((triple5 ((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not green.
False
4
inv-proof
[(((triple5 ((triple7) -> rule3)) -> rule4))]
("Erin" "is" "green" "-")
((triple5 ((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
True
5
proof
[(((((triple5 ((triple7) -> rule3)) -> rule4)) -> rule1))]
("Erin" "is" "quiet" "+")
((((triple5 ((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((((triple5 ((triple7) -> rule3)) -> rule4)) -> rule1))]
("Erin" "is" "quiet" "-")
((((triple5 ((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "rough" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "green" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Bob is green.[(triple3)] Bob is not blue.[(triple2)] Bob is quiet.[(triple4 OR ((triple3) -> rule1))] Erin is big.[(triple5)] Erin is nice.[(triple6)] Erin is rough.[(triple7)] @1: Anne is rough.[(((triple1) -> rule5))] Erin is cold.[(((triple7) -> rule3))] @2: Erin is green.[(((triple5 ((triple7) -> rule3)) -> rule4))] @3: Erin is quiet.[(((((triple5 ((triple7) -> rule3)) -> rule4)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple5 ((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple5 ((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3