Dave is quiet. Dave is red. Gary is big. Gary is cold. Gary is quiet. Gary is red. Gary is smart. Rough things are smart. All smart, cold things are big. Young, red things are smart. Red things are rough. If Dave is big then Dave is young. Smart, rough things are big.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All smart, cold things are big.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Young, red things are smart.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Dave is big then Dave is young.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "young" "+"))
Smart, rough things are big.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Gary is big.
True
1
proof
[(triple3 OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple6) -> rule4)) -> rule6) OR ((((((triple6) -> rule4)) -> rule1) triple4) -> rule2) OR ((((((triple6) -> rule4)) -> rule1) ((triple6) -> rule4)) -> rule6))]
("Gary" "is" "big" "+")
triple3
((triple7 triple4) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple7 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple6) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple6) -> (rule4 % int3))) -> (rule1 % int2)) ((triple6) -> (rule4 % int3))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Gary is rough.
True
2
proof
[(((triple6) -> rule4))]
("Gary" "is" "rough" "+")
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "rough" "-")
((triple2) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
True
6
proof
[(((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6))]
("Dave" "is" "big" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not big.
False
6
inv-proof
[(((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6))]
("Dave" "is" "big" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Dave is quiet.[(triple1)] Dave is red.[(triple2)] Gary is big.[(triple3 OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple6) -> rule4)) -> rule6) OR ((((((triple6) -> rule4)) -> rule1) triple4) -> rule2) OR ((((((triple6) -> rule4)) -> rule1) ((triple6) -> rule4)) -> rule6))] Gary is cold.[(triple4)] Gary is quiet.[(triple5)] Gary is red.[(triple6)] Gary is smart.[(triple7 OR ((((triple6) -> rule4)) -> rule1))] @1: Dave is rough.[(((triple2) -> rule4))] Gary is rough.[(((triple6) -> rule4))] @2: Dave is smart.[(((((triple2) -> rule4)) -> rule1))] @3: Dave is big.[(((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6))] @4: Dave is young.[(((((((((triple2) -> rule4)) -> rule1) ((triple2) -> rule4)) -> rule6)) -> rule5))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
((triple7 triple4) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple7 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple6) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple6) -> (rule4 % int3))) -> (rule1 % int2)) ((triple6) -> (rule4 % int3))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule1 % int3)) ((triple2) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4