Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is round. Bob is smart. Erin is kind. Erin is nice. Erin is red. Erin is round. Erin is smart. Fiona is furry. Fiona is green. Fiona is nice. If someone is round then they are red. Nice people are smart. All furry people are green. All smart people are nice. Smart, red people are kind. Green people are round.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Smart, red people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Erin is kind.
True
1
proof
[(triple8 OR ((triple12 triple10) -> rule5) OR ((triple12 ((triple11) -> rule1)) -> rule5) OR ((((triple9) -> rule2) triple10) -> rule5) OR ((((triple9) -> rule2) ((triple11) -> rule1)) -> rule5))]
("Erin" "is" "kind" "+")
triple8
((triple12 triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple12 ((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple9) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is not nice.
False
1
inv-proof
[(triple15)]
("Fiona" "is" "nice" "-")
triple15
Fiona is smart.
True
2
proof
[(((triple15) -> rule2))]
("Fiona" "is" "smart" "+")
((triple15) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple15) -> rule2))]
("Fiona" "is" "smart" "-")
((triple15) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is red.
True
3
proof
[(((((triple14) -> rule6)) -> rule1) OR ((((((triple13) -> rule3)) -> rule6)) -> rule1))]
("Fiona" "is" "red" "+")
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple13) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not red.
False
3
inv-proof
[(((((triple14) -> rule6)) -> rule1) OR ((((((triple13) -> rule3)) -> rule6)) -> rule1))]
("Fiona" "is" "red" "-")
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple13) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
True
6
proof
[(((((triple15) -> rule2) ((((triple14) -> rule6)) -> rule1)) -> rule5) OR ((((triple15) -> rule2) ((((((triple13) -> rule3)) -> rule6)) -> rule1)) -> rule5))]
("Fiona" "is" "kind" "+")
((((triple15) -> (rule2 % int4)) ((((triple14) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((triple15) -> (rule2 % int5)) ((((((triple13) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Fiona is not kind.
False
6
inv-proof
[(((((triple15) -> rule2) ((((triple14) -> rule6)) -> rule1)) -> rule5) OR ((((triple15) -> rule2) ((((((triple13) -> rule3)) -> rule6)) -> rule1)) -> rule5))]
("Fiona" "is" "kind" "-")
((((triple15) -> (rule2 % int4)) ((((triple14) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((triple15) -> (rule2 % int5)) ((((((triple13) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is green.[(triple2 OR ((triple1) -> rule3))] Bob is kind.[(triple3 OR ((triple7 triple5) -> rule5) OR ((triple7 ((triple6) -> rule1)) -> rule5) OR ((((triple4) -> rule2) triple5) -> rule5) OR ((((triple4) -> rule2) ((triple6) -> rule1)) -> rule5) OR ((triple7 ((((triple2) -> rule6)) -> rule1)) -> rule5) OR ((((triple4) -> rule2) ((((triple2) -> rule6)) -> rule1)) -> rule5) OR ((triple7 ((((((triple1) -> rule3)) -> rule6)) -> rule1)) -> rule5) OR ((((triple4) -> rule2) ((((((triple1) -> rule3)) -> rule6)) -> rule1)) -> rule5))] Bob is nice.[(triple4 OR ((triple7) -> rule4))] Bob is red.[(triple5 OR ((triple6) -> rule1) OR ((((triple2) -> rule6)) -> rule1) OR ((((((triple1) -> rule3)) -> rule6)) -> rule1))] Bob is round.[(triple6 OR ((triple2) -> rule6) OR ((((triple1) -> rule3)) -> rule6))] Bob is smart.[(triple7 OR ((triple4) -> rule2))] Erin is kind.[(triple8 OR ((triple12 triple10) -> rule5) OR ((triple12 ((triple11) -> rule1)) -> rule5) OR ((((triple9) -> rule2) triple10) -> rule5) OR ((((triple9) -> rule2) ((triple11) -> rule1)) -> rule5))] Erin is nice.[(triple9 OR ((triple12) -> rule4))] Erin is red.[(triple10 OR ((triple11) -> rule1))] Erin is round.[(triple11)] Erin is smart.[(triple12 OR ((triple9) -> rule2))] Fiona is furry.[(triple13)] Fiona is green.[(triple14 OR ((triple13) -> rule3))] Fiona is nice.[(triple15)] @1: Fiona is round.[(((triple14) -> rule6) OR ((((triple13) -> rule3)) -> rule6))] Fiona is smart.[(((triple15) -> rule2))] @2: Fiona is red.[(((((triple14) -> rule6)) -> rule1) OR ((((((triple13) -> rule3)) -> rule6)) -> rule1))] @3: Fiona is kind.[(((((triple15) -> rule2) ((((triple14) -> rule6)) -> rule1)) -> rule5) OR ((((triple15) -> rule2) ((((((triple13) -> rule3)) -> rule6)) -> rule1)) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple7 triple5) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple7 ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple4) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((triple7 ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((triple4) -> (rule2 % int4)) ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((triple7 ((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((triple4) -> (rule2 % int5)) ((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple7) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple12 triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple12 ((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple9) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple12) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple10
((triple11) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
((triple9) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
((triple13) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple15
Fiona is round.
("Fiona" "is" "round" "+")
((triple14) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple15) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple13) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple15) -> (rule2 % int4)) ((((triple14) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((triple15) -> (rule2 % int5)) ((((((triple13) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5