Dave is blue. If something is quiet then it is rough. Young things are big. All rough things are cold. If Dave is young then Dave is rough. If Dave is kind and Dave is blue then Dave is young. All blue things are young.
Dave is blue.
("Dave" "is" "blue" "+")
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Dave is young then Dave is rough.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "rough" "+"))
If Dave is kind and Dave is blue then Dave is young.
((("Dave" "is" "kind" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "young" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Dave is young.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "young" "+")
((triple1) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple1) -> rule6))]
("Dave" "is" "young" "-")
((triple1) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Dave" "is" "rough" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("Dave" "is" "big" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
True
4
proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule3))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not cold.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule3))]
("Dave" "is" "cold" "-")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is blue.[(triple1)] @1: Dave is young.[(((triple1) -> rule6))] @2: Dave is big.[(((((triple1) -> rule6)) -> rule2))] Dave is rough.[(((((triple1) -> rule6)) -> rule4))] @3: Dave is cold.[(((((((triple1) -> rule6)) -> rule4)) -> rule3))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3