Bob is blue. Bob is quiet. Bob is white. Gary is blue. Gary is furry. Gary is green. Gary is kind. All blue things are kind. All furry, quiet things are kind. If something is round then it is kind. Kind things are white. If something is white then it is furry. Blue things are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All furry, quiet things are kind.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Gary is blue.
True
1
proof
[(triple4)]
("Gary" "is" "blue" "+")
triple4
Gary is not blue.
False
1
inv-proof
[(triple4)]
("Gary" "is" "blue" "-")
triple4
Bob is furry.
True
2
proof
[(((triple3) -> rule5) OR ((((((triple1) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1) -> rule6)) -> rule4)) -> rule5))]
("Bob" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule6) OR ((((triple3) -> rule5) triple2) -> rule2))]
("Bob" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple1) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is quiet.[(triple2)] Bob is white.[(triple3 OR ((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule6)) -> rule4))] Gary is blue.[(triple4)] Gary is furry.[(triple5 OR ((((triple7) -> rule4)) -> rule5) OR ((((((triple4) -> rule1)) -> rule4)) -> rule5) OR ((((((triple4) -> rule6)) -> rule4)) -> rule5))] Gary is green.[(triple6)] Gary is kind.[(triple7 OR ((triple4) -> rule1) OR ((triple4) -> rule6))] @1: Bob is furry.[(((triple3) -> rule5) OR ((((((triple1) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1) -> rule6)) -> rule4)) -> rule5))] Bob is kind.[(((triple1) -> rule1) OR ((triple1) -> rule6) OR ((((triple3) -> rule5) triple2) -> rule2))] Gary is white.[(((triple7) -> rule4) OR ((((triple4) -> rule1)) -> rule4) OR ((((triple4) -> rule6)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
((triple4) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple4) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple1) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple7) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2