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