Bob is red. Bob is rough. Gary is blue. If Gary is blue then Gary is red. If Gary is rough and Gary is furry then Gary is not smart. All blue, smart things are not white. Rough things are smart. If Bob is white and Bob is not blue then Bob is rough. Blue things are rough.
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If Gary is blue then Gary is red.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "red" "+"))
If Gary is rough and Gary is furry then Gary is not smart.
((("Gary" "is" "rough" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "smart" "-"))
All blue, smart things are not white.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Bob is white and Bob is not blue then Bob is rough.
((("Bob" "is" "white" "+") ("Bob" "is" "blue" "~")) -> ("Bob" "is" "rough" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Bob is rough.
True
1
proof
[(triple2)]
("Bob" "is" "rough" "+")
triple2
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Gary is rough.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "rough" "-")
((triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
True
5
proof
[(((triple3 ((((triple3) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "white" "-")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "white" "+")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is red.[(triple1)] Bob is rough.[(triple2)] Gary is blue.[(triple3)] @1: Bob is smart.[(((triple2) -> rule4))] Gary is red.[(((triple3) -> rule1))] Gary is rough.[(((triple3) -> rule6))] @2: Gary is smart.[(((((triple3) -> rule6)) -> rule4))] @3: Gary is not white.[(((triple3 ((((triple3) -> rule6)) -> rule4)) -> rule3))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3