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