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