Charlie is round. Gary is furry. Gary is quiet. If Charlie is green and Charlie is red then Charlie is big. If someone is big and quiet then they are white. If Gary is red then Gary is green. If Charlie is not red then Charlie is white. All furry people are green. All green, quiet people are big.
Charlie is round.
("Charlie" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Charlie is green and Charlie is red then Charlie is big.
((("Charlie" "is" "green" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "big" "+"))
If someone is big and quiet then they are white.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Gary is red then Gary is green.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "green" "+"))
If Charlie is not red then Charlie is white.
((("Charlie" "is" "red" "~")) -> ("Charlie" "is" "white" "+"))
All furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All green, quiet people are big.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Charlie is not round.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "round" "-")
triple1
Gary is green.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "green" "+")
((triple2) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Gary" "is" "green" "-")
((triple2) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
True
4
proof
[(((((triple2) -> rule5) triple3) -> rule6))]
("Gary" "is" "big" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not big.
False
4
inv-proof
[(((((triple2) -> rule5) triple3) -> rule6))]
("Gary" "is" "big" "-")
((((triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
True
6
proof
[(((((((triple2) -> rule5) triple3) -> rule6) triple3) -> rule2))]
("Gary" "is" "white" "+")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not white.
False
6
inv-proof
[(((((((triple2) -> rule5) triple3) -> rule6) triple3) -> rule2))]
("Gary" "is" "white" "-")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is round.[(triple1)] Gary is furry.[(triple2)] Gary is quiet.[(triple3)] @1: Gary is green.[(((triple2) -> rule5))] @2: Gary is big.[(((((triple2) -> rule5) triple3) -> rule6))] @3: Gary is white.[(((((((triple2) -> rule5) triple3) -> rule6) triple3) -> rule2))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple2) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple2) -> (rule5 % int3)) triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3