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