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