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