Dave is smart. If someone is cold then they are green. If Dave is red and Dave is quiet then Dave is cold. All big people are green. All smart, quiet people are big. If someone is green and quiet then they are cold. Big people are quiet. If someone is big and red then they are green. All smart people are big.
Dave is smart.
("Dave" "is" "smart" "+")
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If Dave is red and Dave is quiet then Dave is cold.
((("Dave" "is" "red" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All smart, quiet people are big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is green and quiet then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big and red then they are green.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Dave is big.
True
2
proof
[(((triple1) -> rule8))]
("Dave" "is" "big" "+")
((triple1) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule8))]
("Dave" "is" "big" "-")
((triple1) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule3))]
("Dave" "is" "green" "-")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
True
7
proof
[(((((((triple1) -> rule8)) -> rule3) ((((triple1) -> rule8)) -> rule6)) -> rule5))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not cold.
False
7
inv-proof
[(((((((triple1) -> rule8)) -> rule3) ((((triple1) -> rule8)) -> rule6)) -> rule5))]
("Dave" "is" "cold" "-")
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is smart.[(triple1)] @1: Dave is big.[(((triple1) -> rule8))] @2: Dave is green.[(((((triple1) -> rule8)) -> rule3))] Dave is quiet.[(((((triple1) -> rule8)) -> rule6))] @3: Dave is cold.[(((((((triple1) -> rule8)) -> rule3) ((((triple1) -> rule8)) -> rule6)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4