Anne is round. Anne is young. Bob is nice. Bob is not young. Erin is blue. Erin is white. Erin is young. All big people are round. If Bob is nice then Bob is blue. If Bob is nice and Bob is big then Bob is white. If someone is nice and not round then they are not young. If someone is big and round then they are red. White people are red. All round, young people are white. If someone is blue and not young then they are white.
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not young.
("Bob" "is" "young" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Bob is nice then Bob is blue.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "blue" "+"))
If Bob is nice and Bob is big then Bob is white.
((("Bob" "is" "nice" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "white" "+"))
If someone is nice and not round then they are not young.
((("someone" "is" "nice" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "-"))
If someone is big and round then they are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All round, young people are white.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is blue and not young then they are white.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "+"))
Erin is young.
True
1
proof
[(triple7)]
("Erin" "is" "young" "+")
triple7
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Bob is blue.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple6) -> rule6))]
("Erin" "is" "red" "-")
((triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Bob is white.
True
4
proof
[(((((triple3) -> rule2) triple4) -> rule8))]
("Bob" "is" "white" "+")
((((triple3) -> (rule2 % int2)) triple4) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1 triple2) -> rule7)) -> rule6))]
("Anne" "is" "red" "-")
((((triple1 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is red.
True
5
proof
[(((((((triple3) -> rule2) triple4) -> rule8)) -> rule6))]
("Bob" "is" "red" "+")
((((((triple3) -> (rule2 % int3)) triple4) -> (rule8 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not red.
False
5
inv-proof
[(((((((triple3) -> rule2) triple4) -> rule8)) -> rule6))]
("Bob" "is" "red" "-")
((((((triple3) -> (rule2 % int3)) triple4) -> (rule8 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is round.[(triple1)] Anne is young.[(triple2)] Bob is nice.[(triple3)] Bob is not young.[(triple4)] Erin is blue.[(triple5)] Erin is white.[(triple6)] Erin is young.[(triple7)] @1: Anne is white.[(((triple1 triple2) -> rule7))] Bob is blue.[(((triple3) -> rule2))] Erin is red.[(((triple6) -> rule6))] @2: Anne is red.[(((((triple1 triple2) -> rule7)) -> rule6))] Bob is white.[(((((triple3) -> rule2) triple4) -> rule8))] @3: Bob is red.[(((((((triple3) -> rule2) triple4) -> rule8)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Anne is white.
("Anne" "is" "white" "+")
((triple1 triple2) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple3) -> (rule2 % int2)) triple4) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((((triple3) -> (rule2 % int3)) triple4) -> (rule8 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3