Charlie is big. Charlie is cold. Charlie is green. Charlie is smart. Gary is big. Gary is green. Gary is not smart. If someone is big then they are cold. All smart, cold people are not nice. If Charlie is smart then Charlie is big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All smart, cold people are not nice.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "-"))
If Charlie is smart then Charlie is big.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "big" "+"))
Gary is big.
True
1
proof
[(triple5)]
("Gary" "is" "big" "+")
triple5
Gary is smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "+")
triple7
Gary is cold.
True
2
proof
[(((triple5) -> rule1))]
("Gary" "is" "cold" "+")
((triple5) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple5) -> rule1))]
("Gary" "is" "cold" "-")
((triple5) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is big.[(triple1 OR ((triple4) -> rule3))] Charlie is cold.[(triple2 OR ((triple1) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] Charlie is green.[(triple3)] Charlie is smart.[(triple4)] Gary is big.[(triple5)] Gary is green.[(triple6)] Gary is not smart.[(triple7)] @1: Charlie is not nice.[(((triple4 triple2) -> rule2) OR ((triple4 ((triple1) -> rule1)) -> rule2) OR ((triple4 ((((triple4) -> rule3)) -> rule1)) -> rule2))] Gary is cold.[(((triple5) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is not smart.
("Gary" "is" "smart" "-")
triple7
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple4 triple2) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
((triple4 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((triple5) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1