Charlie is big. Charlie is furry. Charlie is nice. Charlie is red. Charlie is round. Charlie is smart. Gary is cold. Gary is nice. Gary is round. Gary is smart. Harry is big. Harry is cold. Harry is furry. Harry is red. Harry is smart. Smart people are big. Big people are red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Gary is smart.
True
1
proof
[(triple10)]
("Gary" "is" "smart" "+")
triple10
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Gary is big.
True
2
proof
[(((triple10) -> rule1))]
("Gary" "is" "big" "+")
((triple10) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple10) -> rule1))]
("Gary" "is" "big" "-")
((triple10) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
True
3
proof
[(((((triple10) -> rule1)) -> rule2))]
("Gary" "is" "red" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule2))]
("Gary" "is" "red" "-")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is big.[(triple1 OR ((triple6) -> rule1))] Charlie is furry.[(triple2)] Charlie is nice.[(triple3)] Charlie is red.[(triple4 OR ((triple1) -> rule2) OR ((((triple6) -> rule1)) -> rule2))] Charlie is round.[(triple5)] Charlie is smart.[(triple6)] Gary is cold.[(triple7)] Gary is nice.[(triple8)] Gary is round.[(triple9)] Gary is smart.[(triple10)] Harry is big.[(triple11 OR ((triple15) -> rule1))] Harry is cold.[(triple12)] Harry is furry.[(triple13)] Harry is red.[(triple14 OR ((triple11) -> rule2) OR ((((triple15) -> rule1)) -> rule2))] Harry is smart.[(triple15)] @1: Gary is big.[(((triple10) -> rule1))] @2: Gary is red.[(((((triple10) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple6) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
((triple15) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple11) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Gary is big.
("Gary" "is" "big" "+")
((triple10) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2