Charlie is big. Charlie is green. Charlie is smart. Dave is big. Dave is rough. Dave is smart. Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is round. Gary is smart. All rough things are green.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Gary is rough.
True
1
proof
[(triple10)]
("Gary" "is" "rough" "+")
triple10
Gary is not rough.
False
1
inv-proof
[(triple10)]
("Gary" "is" "rough" "-")
triple10
Dave is green.
True
2
proof
[(((triple5) -> rule1))]
("Dave" "is" "green" "+")
((triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple5) -> rule1))]
("Dave" "is" "green" "-")
((triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2)] Charlie is smart.[(triple3)] Dave is big.[(triple4)] Dave is rough.[(triple5)] Dave is smart.[(triple6)] Gary is green.[(triple7 OR ((triple10) -> rule1))] Gary is quiet.[(triple8)] Gary is red.[(triple9)] Gary is rough.[(triple10)] Gary is round.[(triple11)] Gary is smart.[(triple12)] @1: Dave is green.[(((triple5) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1