Anne is cold. Charlie is cold. Erin is cold. If something is cold then it is smart. If something is smart then it is rough. Cold, rough things are red.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Cold, rough things are red.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Erin is not cold.
False
1
inv-proof
[(triple3)]
("Erin" "is" "cold" "-")
triple3
Anne is smart.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Anne is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is red.
True
5
proof
[(((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "red" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "red" "-")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is cold.[(triple1)] Charlie is cold.[(triple2)] Erin is cold.[(triple3)] @1: Anne is smart.[(((triple1) -> rule1))] Charlie is smart.[(((triple2) -> rule1))] Erin is smart.[(((triple3) -> rule1))] @2: Anne is rough.[(((((triple1) -> rule1)) -> rule2))] Charlie is rough.[(((((triple2) -> rule1)) -> rule2))] Erin is rough.[(((((triple3) -> rule1)) -> rule2))] @3: Anne is red.[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule3))] Charlie is red.[(((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule3))] Erin is red.[(((triple3 ((((triple3) -> rule1)) -> rule2)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3