Anne is quiet. Charlie is big. Erin is not quiet. Gary is round. All smart things are quiet. If Gary is quiet and Gary is young then Gary is smart. All big things are nice. Nice things are smart. If Charlie is not young then Charlie is not smart. Big, round things are not red.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Gary is round.
("Gary" "is" "round" "+")
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Gary is quiet and Gary is young then Gary is smart.
((("Gary" "is" "quiet" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "smart" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Charlie is not young then Charlie is not smart.
((("Charlie" "is" "young" "~")) -> ("Charlie" "is" "smart" "-"))
Big, round things are not red.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Charlie is nice.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("Charlie" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("Charlie" "is" "smart" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
True
4
proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is quiet.[(triple1)] Charlie is big.[(triple2)] Erin is not quiet.[(triple3)] Gary is round.[(triple4)] @1: Charlie is nice.[(((triple2) -> rule3))] @2: Charlie is smart.[(((((triple2) -> rule3)) -> rule4))] @3: Charlie is quiet.[(((((((triple2) -> rule3)) -> rule4)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3