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