Anne is blue. Anne is cold. Dave is big. Dave is quiet. Dave is smart. Dave is young. Erin is big. Erin is blue. Erin is cold. Erin is green. Erin is quiet. Erin is young. If Dave is big then Dave is young. All cold people are young. Big, cold people are not smart. All young people are big. If someone is young and quiet then they are big. If someone is cold and not young then they are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
If Dave is big then Dave is young.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "young" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Big, cold people are not smart.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "-"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is young and quiet then they are big.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and not young then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
Erin is blue.
True
1
proof
[(triple8)]
("Erin" "is" "blue" "+")
triple8
Erin is not blue.
False
1
inv-proof
[(triple8)]
("Erin" "is" "blue" "-")
triple8
Anne is young.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "young" "+")
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is smart.
False
3
inv-proof
[(((triple7 triple9) -> rule3) OR ((((triple12) -> rule4) triple9) -> rule3) OR ((((triple12 triple11) -> rule5) triple9) -> rule3) OR ((((((triple9) -> rule2)) -> rule4) triple9) -> rule3) OR ((((((triple9) -> rule2) triple11) -> rule5) triple9) -> rule3))]
("Erin" "is" "smart" "+")
((triple7 triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
((((triple12) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple12 triple11) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple9) -> (rule2 % int3)) triple11) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Anne is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Anne" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("Anne" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not smart.
True
5
proof
[(((((((triple2) -> rule2)) -> rule4) triple2) -> rule3))]
("Anne" "is" "smart" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
False
5
inv-proof
[(((((((triple2) -> rule2)) -> rule4) triple2) -> rule3))]
("Anne" "is" "smart" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "green" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Dave is big.[(triple3 OR ((triple6) -> rule4) OR ((triple6 triple4) -> rule5))] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Dave is young.[(triple6 OR ((triple3) -> rule1))] Erin is big.[(triple7 OR ((triple12) -> rule4) OR ((triple12 triple11) -> rule5) OR ((((triple9) -> rule2)) -> rule4) OR ((((triple9) -> rule2) triple11) -> rule5))] Erin is blue.[(triple8)] Erin is cold.[(triple9)] Erin is green.[(triple10)] Erin is quiet.[(triple11)] Erin is young.[(triple12 OR ((triple9) -> rule2))] @1: Anne is young.[(((triple2) -> rule2))] Erin is not smart.[(((triple7 triple9) -> rule3) OR ((((triple12) -> rule4) triple9) -> rule3) OR ((((triple12 triple11) -> rule5) triple9) -> rule3) OR ((((((triple9) -> rule2)) -> rule4) triple9) -> rule3) OR ((((((triple9) -> rule2) triple11) -> rule5) triple9) -> rule3))] @2: Anne is big.[(((((triple2) -> rule2)) -> rule4))] @3: Anne is not smart.[(((((((triple2) -> rule2)) -> rule4) triple2) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
((triple6) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
((triple12) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple12 triple11) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple9) -> (rule2 % int2)) triple11) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is not smart.
("Erin" "is" "smart" "-")
((triple7 triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
((((triple12) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple12 triple11) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule4 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((((triple9) -> (rule2 % int3)) triple11) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not smart.
("Anne" "is" "smart" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3