Charlie is red. Charlie is white. Charlie is young. Gary is green. Gary is red. Gary is rough. Gary is round. Gary is white. Gary is young. Harry is green. Harry is quiet. Harry is red. Harry is rough. Harry is round. Harry is white. If someone is young and red then they are round. If someone is round then they are rough. All young, white people are red.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is young and red then they are round.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All young, white people are red.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Gary is young.
True
1
proof
[(triple9)]
("Gary" "is" "young" "+")
triple9
Gary is not rough.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule2) OR ((((triple9 triple5) -> rule1)) -> rule2) OR ((((triple9 ((triple9 triple8) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "rough" "-")
triple6
((triple7) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple9 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple9 ((triple9 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Charlie is round.
True
3
proof
[(((triple3 triple1) -> rule1) OR ((triple3 ((triple3 triple2) -> rule3)) -> rule1))]
("Charlie" "is" "round" "+")
((triple3 triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple3 ((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((triple3 triple1) -> rule1) OR ((triple3 ((triple3 triple2) -> rule3)) -> rule1))]
("Charlie" "is" "round" "-")
((triple3 triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple3 ((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is red.[(triple1 OR ((triple3 triple2) -> rule3))] Charlie is white.[(triple2)] Charlie is young.[(triple3)] Gary is green.[(triple4)] Gary is red.[(triple5 OR ((triple9 triple8) -> rule3))] Gary is rough.[(triple6 OR ((triple7) -> rule2) OR ((((triple9 triple5) -> rule1)) -> rule2) OR ((((triple9 ((triple9 triple8) -> rule3)) -> rule1)) -> rule2))] Gary is round.[(triple7 OR ((triple9 triple5) -> rule1) OR ((triple9 ((triple9 triple8) -> rule3)) -> rule1))] Gary is white.[(triple8)] Gary is young.[(triple9)] Harry is green.[(triple10)] Harry is quiet.[(triple11)] Harry is red.[(triple12)] Harry is rough.[(triple13 OR ((triple14) -> rule2))] Harry is round.[(triple14)] Harry is white.[(triple15)] @1: Charlie is round.[(((triple3 triple1) -> rule1) OR ((triple3 ((triple3 triple2) -> rule3)) -> rule1))] @2: Charlie is rough.[(((((triple3 triple1) -> rule1)) -> rule2) OR ((((triple3 ((triple3 triple2) -> rule3)) -> rule1)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
((triple3 triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple9 triple8) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple7) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple9 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple9 ((triple9 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple7
((triple9 triple5) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple9 ((triple9 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple8
Gary is young.
("Gary" "is" "young" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
((triple14) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Charlie is round.
("Charlie" "is" "round" "+")
((triple3 triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple3 ((triple3 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple3 ((triple3 triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3