Dave is red. Harry is cold. All red people are cold. If someone is red then they are quiet. Cold people are red. If Harry is green then Harry is cold. If Harry is green then Harry is red. All quiet people are smart.
Dave is red.
("Dave" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Harry is green then Harry is cold.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "cold" "+"))
If Harry is green then Harry is red.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "red" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("Harry" "is" "red" "-")
((triple2) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule6))]
("Harry" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule6))]
("Harry" "is" "smart" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Dave is red.[(triple1)] Harry is cold.[(triple2)] @1: Dave is cold.[(((triple1) -> rule1))] Dave is quiet.[(((triple1) -> rule2))] Harry is red.[(((triple2) -> rule3))] @2: Dave is smart.[(((((triple1) -> rule2)) -> rule6))] Harry is quiet.[(((((triple2) -> rule3)) -> rule2))] @3: Harry is smart.[(((((((triple2) -> rule3)) -> rule2)) -> rule6))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3