Anne is blue. Anne is quiet. Charlie is young. Blue people are round. Round, young people are quiet. All kind people are blue. If Charlie is red and Charlie is kind then Charlie is furry. If someone is furry and kind then they are young. If Charlie is young then Charlie is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Round, young people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is red and Charlie is kind then Charlie is furry.
((("Charlie" "is" "red" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "furry" "+"))
If someone is furry and kind then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Charlie is young then Charlie is blue.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "blue" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple2)]
("Anne" "is" "quiet" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Charlie" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Charlie" "is" "round" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
True
5
proof
[(((((((triple3) -> rule6)) -> rule1) triple3) -> rule2))]
("Charlie" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not quiet.
False
5
inv-proof
[(((((((triple3) -> rule6)) -> rule1) triple3) -> rule2))]
("Charlie" "is" "quiet" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "furry" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "young" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2)] Charlie is young.[(triple3)] @1: Anne is round.[(((triple1) -> rule1))] Charlie is blue.[(((triple3) -> rule6))] @2: Charlie is round.[(((((triple3) -> rule6)) -> rule1))] @3: Charlie is quiet.[(((((((triple3) -> rule6)) -> rule1) triple3) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3