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