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