Anne is quiet. Bob is round. Charlie is quiet. Gary is big. If Charlie is nice and Charlie is big then Charlie is young. All quiet people are young. Quiet people are not nice. If someone is cold then they are quiet. If Anne is not nice then Anne is big. All cold, big people are round. If Bob is cold and Bob is round then Bob is young. Big people are not kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
If Charlie is nice and Charlie is big then Charlie is young.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "young" "+"))
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Quiet people are not nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is not nice then Anne is big.
((("Anne" "is" "nice" "~")) -> ("Anne" "is" "big" "+"))
All cold, big people are round.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Bob is cold and Bob is round then Bob is young.
((("Bob" "is" "cold" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
Big people are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Charlie is not nice.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Gary is kind.
False
2
inv-proof
[(((triple4) -> rule8))]
("Gary" "is" "kind" "+")
((triple4) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is not kind.
True
4
proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule8))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
int3
Anne is kind.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule5)) -> rule8))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "+")
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Bob is round.[(triple2)] Charlie is quiet.[(triple3)] Gary is big.[(triple4)] @1: Anne is not nice.[(((triple1) -> rule3))] Anne is young.[(((triple1) -> rule2))] Charlie is not nice.[(((triple3) -> rule3))] Charlie is young.[(((triple3) -> rule2))] Gary is not kind.[(((triple4) -> rule8))] @2: Anne is big.[(((((triple1) -> rule3)) -> rule5))] @3: Anne is not kind.[(((((((triple1) -> rule3)) -> rule5)) -> rule8))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Anne is not nice.
("Anne" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
((triple4) -> (rule8 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is not kind.
("Anne" "is" "kind" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
int3