Bob is kind. Bob is nice. Bob is red. Bob is white. Charlie is kind. Charlie is nice. Charlie is red. Charlie is round. Fiona is round. Fiona is smart. If Fiona is nice and Fiona is smart then Fiona is round. All white things are kind. White, kind things are nice. White, red things are kind. Red, smart things are green. If something is kind then it is smart. All round things are kind. If something is round then it is white.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Fiona is nice and Fiona is smart then Fiona is round.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "round" "+"))
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
White, kind things are nice.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
White, red things are kind.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Red, smart things are green.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Bob is nice.
True
1
proof
[(triple2 OR ((triple4 triple1) -> rule3) OR ((triple4 ((triple4) -> rule2)) -> rule3) OR ((triple4 ((triple4 triple3) -> rule4)) -> rule3))]
("Bob" "is" "nice" "+")
triple2
((triple4 triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple4 ((triple4 triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not red.
False
1
inv-proof
[(triple3)]
("Bob" "is" "red" "-")
triple3
Fiona is white.
True
2
proof
[(((triple9) -> rule8))]
("Fiona" "is" "white" "+")
((triple9) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule6) OR ((((triple4) -> rule2)) -> rule6) OR ((((triple4 triple3) -> rule4)) -> rule6))]
("Bob" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple4 triple3) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is green.
True
4
proof
[(((triple7 ((triple5) -> rule6)) -> rule5) OR ((triple7 ((((triple8) -> rule7)) -> rule6)) -> rule5) OR ((triple7 ((((((triple8) -> rule8)) -> rule2)) -> rule6)) -> rule5) OR ((triple7 ((((((triple8) -> rule8) triple7) -> rule4)) -> rule6)) -> rule5))]
("Charlie" "is" "green" "+")
((triple7 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((triple7 ((((triple8) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((triple7 ((((((triple8) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((triple7 ((((((triple8) -> (rule8 % int4)) triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Fiona is not nice.
False
5
inv-proof
[(((((triple9) -> rule8) ((triple9) -> rule7)) -> rule3) OR ((((triple9) -> rule8) ((((triple9) -> rule8)) -> rule2)) -> rule3))]
("Fiona" "is" "nice" "-")
((((triple9) -> (rule8 % int3)) ((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((triple9) -> (rule8 % int3)) ((((triple9) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is kind.[(triple1 OR ((triple4) -> rule2) OR ((triple4 triple3) -> rule4))] Bob is nice.[(triple2 OR ((triple4 triple1) -> rule3) OR ((triple4 ((triple4) -> rule2)) -> rule3) OR ((triple4 ((triple4 triple3) -> rule4)) -> rule3))] Bob is red.[(triple3)] Bob is white.[(triple4)] Charlie is kind.[(triple5 OR ((triple8) -> rule7) OR ((((triple8) -> rule8)) -> rule2) OR ((((triple8) -> rule8) triple7) -> rule4))] Charlie is nice.[(triple6 OR ((((triple8) -> rule8) triple5) -> rule3) OR ((((triple8) -> rule8) ((triple8) -> rule7)) -> rule3) OR ((((triple8) -> rule8) ((((triple8) -> rule8)) -> rule2)) -> rule3) OR ((((triple8) -> rule8) ((((triple8) -> rule8) triple7) -> rule4)) -> rule3))] Charlie is red.[(triple7)] Charlie is round.[(triple8)] Fiona is round.[(triple9)] Fiona is smart.[(triple10 OR ((((triple9) -> rule7)) -> rule6) OR ((((((triple9) -> rule8)) -> rule2)) -> rule6))] @1: Bob is smart.[(((triple1) -> rule6) OR ((((triple4) -> rule2)) -> rule6) OR ((((triple4 triple3) -> rule4)) -> rule6))] Charlie is smart.[(((triple5) -> rule6) OR ((((triple8) -> rule7)) -> rule6) OR ((((((triple8) -> rule8)) -> rule2)) -> rule6) OR ((((((triple8) -> rule8) triple7) -> rule4)) -> rule6))] Charlie is white.[(((triple8) -> rule8))] Fiona is kind.[(((triple9) -> rule7) OR ((((triple9) -> rule8)) -> rule2))] Fiona is white.[(((triple9) -> rule8))] @2: Bob is green.[(((triple3 ((triple1) -> rule6)) -> rule5) OR ((triple3 ((((triple4) -> rule2)) -> rule6)) -> rule5) OR ((triple3 ((((triple4 triple3) -> rule4)) -> rule6)) -> rule5))] Charlie is green.[(((triple7 ((triple5) -> rule6)) -> rule5) OR ((triple7 ((((triple8) -> rule7)) -> rule6)) -> rule5) OR ((triple7 ((((((triple8) -> rule8)) -> rule2)) -> rule6)) -> rule5) OR ((triple7 ((((((triple8) -> rule8) triple7) -> rule4)) -> rule6)) -> rule5))] Fiona is nice.[(((((triple9) -> rule8) ((triple9) -> rule7)) -> rule3) OR ((((triple9) -> rule8) ((((triple9) -> rule8)) -> rule2)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((triple4) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple4 triple3) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple4 triple1) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple4 ((triple4 triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
((triple8) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple8) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple8) -> (rule8 % int2)) triple7) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((((triple8) -> (rule8 % int2)) triple5) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple8) -> (rule8 % int3)) ((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple8) -> (rule8 % int3)) ((((triple8) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple8) -> (rule8 % int3)) ((((triple8) -> (rule8 % int3)) triple7) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((((triple9) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple9) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple4 triple3) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple8) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple8) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple8) -> (rule8 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple8) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple9) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple3 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((triple3 ((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((triple3 ((((triple4 triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((triple7 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((triple7 ((((triple8) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((triple7 ((((((triple8) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((triple7 ((((((triple8) -> (rule8 % int4)) triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple9) -> (rule8 % int3)) ((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((((triple9) -> (rule8 % int3)) ((((triple9) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3