Charlie is blue. Charlie is kind. Charlie is not red. Charlie is not smart. Charlie is young. Dave is big. Dave is blue. Dave is kind. Dave is not nice. Dave is smart. Dave is young. Harry is big. Harry is blue. Harry is kind. Harry is nice. Harry is smart. If something is smart and red then it is young. All nice things are young. All nice, blue things are young. If Charlie is not big then Charlie is not young. All big, young things are red. Young, big things are blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and red then it is young.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All nice, blue things are young.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If Charlie is not big then Charlie is not young.
((("Charlie" "is" "big" "~")) -> ("Charlie" "is" "young" "-"))
All big, young things are red.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Young, big things are blue.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Dave is kind.
True
1
proof
[(triple8)]
("Dave" "is" "kind" "+")
triple8
Harry is not smart.
False
1
inv-proof
[(triple16)]
("Harry" "is" "smart" "-")
triple16
Dave is red.
True
3
proof
[(((triple6 triple11) -> rule5))]
("Dave" "is" "red" "+")
((triple6 triple11) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple15) -> rule2) OR ((triple15 triple13) -> rule3))]
("Harry" "is" "young" "-")
((triple15) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple15 triple13) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
True
4
proof
[(((triple12 ((triple15) -> rule2)) -> rule5) OR ((triple12 ((triple15 triple13) -> rule3)) -> rule5))]
("Harry" "is" "red" "+")
((triple12 ((triple15) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple12 ((triple15 triple13) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not red.
False
4
inv-proof
[(((triple12 ((triple15) -> rule2)) -> rule5) OR ((triple12 ((triple15 triple13) -> rule3)) -> rule5))]
("Harry" "is" "red" "-")
((triple12 ((triple15) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple12 ((triple15 triple13) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2)] Charlie is not red.[(triple3)] Charlie is not smart.[(triple4)] Charlie is young.[(triple5)] Dave is big.[(triple6)] Dave is blue.[(triple7 OR ((triple11 triple6) -> rule6))] Dave is kind.[(triple8)] Dave is not nice.[(triple9)] Dave is smart.[(triple10)] Dave is young.[(triple11)] Harry is big.[(triple12)] Harry is blue.[(triple13 OR ((((triple15) -> rule2) triple12) -> rule6))] Harry is kind.[(triple14)] Harry is nice.[(triple15)] Harry is smart.[(triple16)] @1: Dave is red.[(((triple6 triple11) -> rule5))] Harry is young.[(((triple15) -> rule2) OR ((triple15 triple13) -> rule3))] @2: Harry is red.[(((triple12 ((triple15) -> rule2)) -> rule5) OR ((triple12 ((triple15 triple13) -> rule3)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is not red.
("Charlie" "is" "red" "-")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
((triple11 triple6) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is not nice.
("Dave" "is" "nice" "-")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
((((triple15) -> (rule2 % int2)) triple12) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Dave is red.
("Dave" "is" "red" "+")
((triple6 triple11) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple15) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple15 triple13) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12 ((triple15) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple12 ((triple15 triple13) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2