Charlie is cold. Dave is big. Dave is cold. If something is young then it is quiet. If Dave is quiet then Dave is red. All cold things are young.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Dave is quiet then Dave is red.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "red" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Charlie is young.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "young" "+")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "young" "-")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Dave is red.
True
4
proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "red" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not red.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "red" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is cold.[(triple1)] Dave is big.[(triple2)] Dave is cold.[(triple3)] @1: Charlie is young.[(((triple1) -> rule3))] Dave is young.[(((triple3) -> rule3))] @2: Charlie is quiet.[(((((triple1) -> rule3)) -> rule1))] Dave is quiet.[(((((triple3) -> rule3)) -> rule1))] @3: Dave is red.[(((((((triple3) -> rule3)) -> rule1)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3