Anne is nice. Bob is big. Bob is blue. Bob is cold. Bob is nice. Bob is red. Erin is big. Erin is cold. Erin is kind. Erin is nice. If someone is red and cold then they are blue. Red, kind people are round. Nice people are kind. If Erin is nice then Erin is blue. If someone is nice then they are blue. If someone is kind and round then they are red. Red people are round. Nice, kind people are round.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is red and cold then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Red, kind people are round.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If Erin is nice then Erin is blue.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "blue" "+"))
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and round then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Nice, kind people are round.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Bob is nice.
True
1
proof
[(triple5)]
("Bob" "is" "nice" "+")
triple5
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Bob is big.[(triple2)] Bob is blue.[(triple3 OR ((triple5) -> rule5) OR ((triple6 triple4) -> rule1) OR ((((((triple5) -> rule3) ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule6) triple4) -> rule1))] Bob is cold.[(triple4)] Bob is nice.[(triple5)] Bob is red.[(triple6 OR ((((triple5) -> rule3) ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule6))] Erin is big.[(triple7)] Erin is cold.[(triple8)] Erin is kind.[(triple9 OR ((triple10) -> rule3))] Erin is nice.[(triple10)] @1: Anne is blue.[(((triple1) -> rule5))] Anne is kind.[(((triple1) -> rule3))] Bob is kind.[(((triple5) -> rule3))] Bob is round.[(((triple6) -> rule7) OR ((triple5 ((triple5) -> rule3)) -> rule8) OR ((triple6 ((triple5) -> rule3)) -> rule2))] Erin is blue.[(((triple10) -> rule4) OR ((triple10) -> rule5) OR ((((triple9 ((triple10 triple9) -> rule8)) -> rule6) triple8) -> rule1) OR ((((((triple10) -> rule3) ((triple10 triple9) -> rule8)) -> rule6) triple8) -> rule1) OR ((((triple9 ((triple10 ((triple10) -> rule3)) -> rule8)) -> rule6) triple8) -> rule1) OR ((((((triple10) -> rule3) ((triple10 ((triple10) -> rule3)) -> rule8)) -> rule6) triple8) -> rule1))] Erin is round.[(((triple10 triple9) -> rule8) OR ((triple10 ((triple10) -> rule3)) -> rule8))] @2: Anne is round.[(((triple1 ((triple1) -> rule3)) -> rule8))] Erin is red.[(((triple9 ((triple10 triple9) -> rule8)) -> rule6) OR ((((triple10) -> rule3) ((triple10 triple9) -> rule8)) -> rule6) OR ((triple9 ((triple10 ((triple10) -> rule3)) -> rule8)) -> rule6) OR ((((triple10) -> rule3) ((triple10 ((triple10) -> rule3)) -> rule8)) -> rule6))] @3: Anne is red.[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule8)) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
((triple5) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((((triple5) -> (rule3 % int4)) ((triple5 ((triple5) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
((((triple5) -> (rule3 % int3)) ((triple5 ((triple5) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
((triple10) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple6) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple6 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple10) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple10) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple9 ((triple10 triple9) -> (rule8 % int3))) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple10) -> (rule3 % int4)) ((triple10 triple9) -> (rule8 % int3))) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((triple9 ((triple10 ((triple10) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((triple10) -> (rule3 % int4)) ((triple10 ((triple10) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
((triple10 triple9) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple9 ((triple10 triple9) -> (rule8 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple10 triple9) -> (rule8 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((triple9 ((triple10 ((triple10) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple10) -> (rule3 % int3)) ((triple10 ((triple10) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3