Gary is cold. Smart things are big. If something is smart and furry then it is red. Smart, nice things are red. All big things are nice. If Gary is furry and Gary is blue then Gary is nice. If something is furry then it is cold. If something is furry then it is smart. If Gary is cold then Gary is smart.
Gary is cold.
("Gary" "is" "cold" "+")
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is smart and furry then it is red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Smart, nice things are red.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Gary is furry and Gary is blue then Gary is nice.
((("Gary" "is" "furry" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "nice" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Gary is cold then Gary is smart.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "+"))
Gary is cold.
True
1
proof
[(triple1)]
("Gary" "is" "cold" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple1)]
("Gary" "is" "cold" "-")
triple1
Gary is smart.
True
2
proof
[(((triple1) -> rule8))]
("Gary" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple1) -> rule8))]
("Gary" "is" "smart" "-")
((triple1) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
True
3
proof
[(((((triple1) -> rule8)) -> rule1))]
("Gary" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule1))]
("Gary" "is" "big" "-")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Gary is cold.[(triple1)] @1: Gary is smart.[(((triple1) -> rule8))] @2: Gary is big.[(((((triple1) -> rule8)) -> rule1))] @3: Gary is nice.[(((((((triple1) -> rule8)) -> rule1)) -> rule4))] @4: Gary is red.[(((((triple1) -> rule8) ((((((triple1) -> rule8)) -> rule1)) -> rule4)) -> rule3))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is smart.
("Gary" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple1) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple1) -> (rule8 % int4)) ((((((triple1) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4