Anne is blue. Anne is cold. Anne is not green. Bob is cold. Charlie is blue. Dave is not blue. Dave is cold. If Anne is rough then Anne is big. If Dave is not cold then Dave is young. Rough, young people are not red. All blue people are rough. If Anne is big and Anne is green then Anne is blue. Big, cold people are blue. If someone is red and green then they are young. Big people are not young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not green.
("Anne" "is" "green" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is cold.
("Dave" "is" "cold" "+")
If Anne is rough then Anne is big.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "big" "+"))
If Dave is not cold then Dave is young.
((("Dave" "is" "cold" "~")) -> ("Dave" "is" "young" "+"))
Rough, young people are not red.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "-"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Anne is big and Anne is green then Anne is blue.
((("Anne" "is" "big" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "blue" "+"))
Big, cold people are blue.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and green then they are young.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Big people are not young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "-"))
Anne is not green.
True
1
proof
[(triple3)]
("Anne" "is" "green" "-")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "blue" "-")
triple5
Anne is rough.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple5) -> rule4))]
("Charlie" "is" "rough" "-")
((triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not young.
True
4
proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule8))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is young.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule8))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "young" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "young" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is not green.[(triple3)] Bob is cold.[(triple4)] Charlie is blue.[(triple5)] Dave is cold.[(triple7)] Dave is not blue.[(triple6)] @1: Anne is rough.[(((triple1) -> rule4))] Charlie is rough.[(((triple5) -> rule4))] @2: Anne is big.[(((((triple1) -> rule4)) -> rule1))] @3: Anne is not young.[(((((((triple1) -> rule4)) -> rule1)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not green.
("Anne" "is" "green" "-")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is not blue.
("Dave" "is" "blue" "-")
triple6
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not young.
("Anne" "is" "young" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3