Gary is big. Gary is blue. Gary is green. Gary is kind. Gary is quiet. Gary is rough. Gary is round. Harry is big. Harry is green. Harry is kind. Harry is quiet. Harry is rough. If something is rough then it is green. If something is round and big then it is green. If something is big then it is green. All round, big things are green. If something is rough and not big then it is quiet. If Gary is rough and Gary is not quiet then Gary is green. All round things are kind. All green, blue things are kind.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is round and big then it is green.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All round, big things are green.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is rough and not big then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "big" "~")) -> ("something" "is" "quiet" "+"))
If Gary is rough and Gary is not quiet then Gary is green.
((("Gary" "is" "rough" "+") ("Gary" "is" "quiet" "~")) -> ("Gary" "is" "green" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All green, blue things are kind.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Harry is rough.
True
1
proof
[(triple12)]
("Harry" "is" "rough" "+")
triple12
Harry is not big.
False
1
inv-proof
[(triple8)]
("Harry" "is" "big" "-")
triple8
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Gary is big.[(triple1)] Gary is blue.[(triple2)] Gary is green.[(triple3 OR ((triple1) -> rule3) OR ((triple6) -> rule1) OR ((triple7 triple1) -> rule2) OR ((triple7 triple1) -> rule4))] Gary is kind.[(triple4 OR ((triple7) -> rule7) OR ((triple3 triple2) -> rule8) OR ((((triple1) -> rule3) triple2) -> rule8) OR ((((triple6) -> rule1) triple2) -> rule8) OR ((((triple7 triple1) -> rule2) triple2) -> rule8) OR ((((triple7 triple1) -> rule4) triple2) -> rule8))] Gary is quiet.[(triple5)] Gary is rough.[(triple6)] Gary is round.[(triple7)] Harry is big.[(triple8)] Harry is green.[(triple9 OR ((triple12) -> rule1) OR ((triple8) -> rule3))] Harry is kind.[(triple10)] Harry is quiet.[(triple11)] Harry is rough.[(triple12)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
((triple1) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple6) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple7 triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple7 triple1) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple4
((triple7) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple3 triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple6) -> (rule1 % int2)) triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple7 triple1) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple7 triple1) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple12) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple8) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12