Charlie is big. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is kind. Gary is big. Gary is kind. Gary is red. Gary is smart. Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is red. Harry is smart. All kind people are furry. Big, smart people are furry. If someone is furry then they are red. If Harry is furry then Harry is big. If Gary is smart and Gary is furry then Gary is cold. If someone is furry then they are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Big, smart people are furry.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If Harry is furry then Harry is big.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "big" "+"))
If Gary is smart and Gary is furry then Gary is cold.
((("Gary" "is" "smart" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "cold" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Gary is kind.
True
1
proof
[(triple7)]
("Gary" "is" "kind" "+")
triple7
Gary is not big.
False
1
inv-proof
[(triple6 OR ((((triple7) -> rule1)) -> rule6))]
("Gary" "is" "big" "-")
triple6
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Charlie is big.[(triple1 OR ((triple4) -> rule6) OR ((((triple5) -> rule1)) -> rule6))] Charlie is blue.[(triple2)] Charlie is cold.[(triple3)] Charlie is furry.[(triple4 OR ((triple5) -> rule1))] Charlie is kind.[(triple5)] Gary is big.[(triple6 OR ((((triple7) -> rule1)) -> rule6))] Gary is kind.[(triple7)] Gary is red.[(triple8 OR ((((triple7) -> rule1)) -> rule3) OR ((((triple6 triple9) -> rule2)) -> rule3))] Gary is smart.[(triple9)] Harry is big.[(triple10 OR ((triple13) -> rule4) OR ((triple13) -> rule6))] Harry is blue.[(triple11)] Harry is cold.[(triple12)] Harry is furry.[(triple13 OR ((triple10 triple15) -> rule2))] Harry is red.[(triple14 OR ((triple13) -> rule3) OR ((((triple10 triple15) -> rule2)) -> rule3))] Harry is smart.[(triple15)] @1: Charlie is red.[(((triple4) -> rule3) OR ((((triple5) -> rule1)) -> rule3))] Gary is furry.[(((triple7) -> rule1) OR ((triple6 triple9) -> rule2))] @2: Gary is cold.[(((triple9 ((triple7) -> rule1)) -> rule5) OR ((triple9 ((triple6 triple9) -> rule2)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
((triple5) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple13) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple13) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((triple10 triple15) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple13) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple10 triple15) -> (rule2 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple7) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple6 triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple9 ((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple9 ((triple6 triple9) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2