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