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