Bob is green. Bob is nice. Bob is round. Bob is white. Dave is not nice. Dave is round. Dave is white. Erin is nice. Erin is round. Erin is white. If Bob is cold and Bob is not nice then Bob is round. If someone is nice and round then they are not cold. If someone is green and not round then they are red. If someone is red and not cold then they are smart. All smart people are green. If Erin is round and Erin is not cold then Erin is red. If someone is nice and smart then they are white. Red people are white.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
If Bob is cold and Bob is not nice then Bob is round.
((("Bob" "is" "cold" "+") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "round" "+"))
If someone is nice and round then they are not cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
If someone is green and not round then they are red.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
If someone is red and not cold then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "smart" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Erin is round and Erin is not cold then Erin is red.
((("Erin" "is" "round" "+") ("Erin" "is" "cold" "~")) -> ("Erin" "is" "red" "+"))
If someone is nice and smart then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Erin is round.
True
1
proof
[(triple9)]
("Erin" "is" "round" "+")
triple9
Dave is not white.
False
1
inv-proof
[(triple7)]
("Dave" "is" "white" "-")
triple7
Erin is not cold.
True
3
proof
[(((triple8 triple9) -> rule2))]
("Erin" "is" "cold" "-")
((triple8 triple9) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is cold.
False
3
inv-proof
[(((triple8 triple9) -> rule2))]
("Erin" "is" "cold" "+")
((triple8 triple9) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is red.
True
5
proof
[(((triple9 ((triple8 triple9) -> rule2)) -> rule6))]
("Erin" "is" "red" "+")
((triple9 ((triple8 triple9) -> (rule2 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
int2
Erin is not red.
False
5
inv-proof
[(((triple9 ((triple8 triple9) -> rule2)) -> rule6))]
("Erin" "is" "red" "-")
((triple9 ((triple8 triple9) -> (rule2 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
int2
Erin is smart.
True
9
proof
[(((((triple9 ((triple8 triple9) -> rule2)) -> rule6) ((triple8 triple9) -> rule2)) -> rule4))]
("Erin" "is" "smart" "+")
((((triple9 ((triple8 triple9) -> (rule2 % int3))) -> (rule6 % int2)) ((triple8 triple9) -> (rule2 % int3))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
Erin is not smart.
False
9
inv-proof
[(((((triple9 ((triple8 triple9) -> rule2)) -> rule6) ((triple8 triple9) -> rule2)) -> rule4))]
("Erin" "is" "smart" "-")
((((triple9 ((triple8 triple9) -> (rule2 % int3))) -> (rule6 % int2)) ((triple8 triple9) -> (rule2 % int3))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is green.[(triple1)] Bob is nice.[(triple2)] Bob is round.[(triple3)] Bob is white.[(triple4)] Dave is not nice.[(triple5)] Dave is round.[(triple6)] Dave is white.[(triple7)] Erin is nice.[(triple8)] Erin is round.[(triple9)] Erin is white.[(triple10 OR ((((triple9 ((triple8 triple9) -> rule2)) -> rule6)) -> rule8) OR ((triple8 ((((triple9 ((triple8 triple9) -> rule2)) -> rule6) ((triple8 triple9) -> rule2)) -> rule4)) -> rule7))] @1: Bob is not cold.[(((triple2 triple3) -> rule2))] Erin is not cold.[(((triple8 triple9) -> rule2))] @2: Erin is red.[(((triple9 ((triple8 triple9) -> rule2)) -> rule6))] @3: Erin is smart.[(((((triple9 ((triple8 triple9) -> rule2)) -> rule6) ((triple8 triple9) -> rule2)) -> rule4))] @4: Erin is green.[(((((((triple9 ((triple8 triple9) -> rule2)) -> rule6) ((triple8 triple9) -> rule2)) -> rule4)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
((((triple9 ((triple8 triple9) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
((triple8 ((((triple9 ((triple8 triple9) -> (rule2 % int4))) -> (rule6 % int3)) ((triple8 triple9) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
int4
Bob is not cold.
("Bob" "is" "cold" "-")
((triple2 triple3) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
((triple8 triple9) -> (rule2 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple9 ((triple8 triple9) -> (rule2 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple9 ((triple8 triple9) -> (rule2 % int3))) -> (rule6 % int2)) ((triple8 triple9) -> (rule2 % int3))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple9 ((triple8 triple9) -> (rule2 % int4))) -> (rule6 % int3)) ((triple8 triple9) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not cold.
("Erin" "is" "cold" "-")
int4