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