Anne is cold. Anne is red. Anne is rough. Anne is smart. Charlie is cold. Charlie is green. Charlie is smart. Charlie is young. Erin is cold. Erin is red. Erin is rough. Erin is young. If something is smart then it is young. Smart, big things are cold. If Anne is young then Anne is green. If something is smart then it is rough. If something is young and big then it is smart. If something is cold and young then it is rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Smart, big things are cold.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Anne is young then Anne is green.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "green" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is young and big then it is smart.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is cold and young then it is rough.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Erin is rough.
True
1
proof
[(triple11 OR ((triple9 triple12) -> rule6))]
("Erin" "is" "rough" "+")
triple11
((triple9 triple12) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Charlie is not green.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "green" "-")
triple6
Charlie is rough.
True
2
proof
[(((triple7) -> rule4) OR ((triple5 triple8) -> rule6) OR ((triple5 ((triple7) -> rule1)) -> rule6))]
("Charlie" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 triple8) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Anne is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Anne" "is" "young" "-")
((triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("Anne" "is" "green" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("Anne" "is" "green" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Anne is rough.[(triple3 OR ((triple4) -> rule4) OR ((triple1 ((triple4) -> rule1)) -> rule6))] Anne is smart.[(triple4)] Charlie is cold.[(triple5)] Charlie is green.[(triple6)] Charlie is smart.[(triple7)] Charlie is young.[(triple8 OR ((triple7) -> rule1))] Erin is cold.[(triple9)] Erin is red.[(triple10)] Erin is rough.[(triple11 OR ((triple9 triple12) -> rule6))] Erin is young.[(triple12)] @1: Anne is young.[(((triple4) -> rule1))] Charlie is rough.[(((triple7) -> rule4) OR ((triple5 triple8) -> rule6) OR ((triple5 ((triple7) -> rule1)) -> rule6))] @2: Anne is green.[(((((triple4) -> rule1)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple7) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
((triple9 triple12) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple12
Anne is young.
("Anne" "is" "young" "+")
((triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 triple8) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2