Bob is cold. Bob is furry. Bob is round. Bob is white. Charlie is blue. Charlie is quiet. Charlie is round. Erin is blue. Erin is furry. Erin is green. Erin is round. Erin is white. If Erin is blue and Erin is white then Erin is round. If someone is quiet then they are green. If someone is quiet then they are green. Green people are round. If someone is white and quiet then they are blue. All round, cold people are blue. All quiet, cold people are white. If Erin is furry then Erin is white.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
If Erin is blue and Erin is white then Erin is round.
((("Erin" "is" "blue" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "round" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet then they are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is white and quiet then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All round, cold people are blue.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All quiet, cold people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Erin is furry then Erin is white.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "white" "+"))
Charlie is round.
True
1
proof
[(triple7 OR ((((triple6) -> rule2)) -> rule4) OR ((((triple6) -> rule3)) -> rule4))]
("Charlie" "is" "round" "+")
triple7
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not round.
False
1
inv-proof
[(triple7 OR ((((triple6) -> rule2)) -> rule4) OR ((((triple6) -> rule3)) -> rule4))]
("Charlie" "is" "round" "-")
triple7
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Bob is blue.
True
3
proof
[(((triple3 triple1) -> rule6))]
("Bob" "is" "blue" "+")
((triple3 triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple6) -> rule2) OR ((triple6) -> rule3))]
("Charlie" "is" "green" "-")
((triple6) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple6) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is round.[(triple3)] Bob is white.[(triple4)] Charlie is blue.[(triple5)] Charlie is quiet.[(triple6)] Charlie is round.[(triple7 OR ((((triple6) -> rule2)) -> rule4) OR ((((triple6) -> rule3)) -> rule4))] Erin is blue.[(triple8)] Erin is furry.[(triple9)] Erin is green.[(triple10)] Erin is round.[(triple11 OR ((triple10) -> rule4) OR ((triple8 triple12) -> rule1) OR ((triple8 ((triple9) -> rule8)) -> rule1))] Erin is white.[(triple12 OR ((triple9) -> rule8))] @1: Bob is blue.[(((triple3 triple1) -> rule6))] Charlie is green.[(((triple6) -> rule2) OR ((triple6) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple10) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple8 triple12) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple8 ((triple9) -> (rule8 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple9) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple6) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple6) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1