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