Bob is blue. Charlie is rough. Dave is blue. Dave is nice. Erin is nice. Erin is red. Erin is rough. All rough people are furry. Rough, nice people are blue. If someone is cold then they are furry. Kind people are cold. If Charlie is nice and Charlie is blue then Charlie is red. All blue people are kind. All furry people are nice.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Rough, nice people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is nice and Charlie is blue then Charlie is red.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "red" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Erin is red.
True
1
proof
[(triple6)]
("Erin" "is" "red" "+")
triple6
Erin is not nice.
False
1
inv-proof
[(triple5 OR ((((triple7) -> rule1)) -> rule7))]
("Erin" "is" "nice" "-")
triple5
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Dave is kind.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is not blue.
False
3
inv-proof
[(((triple7 triple5) -> rule2) OR ((triple7 ((((triple7) -> rule1)) -> rule7)) -> rule2))]
("Erin" "is" "blue" "-")
((triple7 triple5) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is nice.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("Charlie" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((((triple7 triple5) -> rule2)) -> rule6) OR ((((triple7 ((((triple7) -> rule1)) -> rule7)) -> rule2)) -> rule6))]
("Erin" "is" "kind" "-")
((((triple7 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple7 ((((triple7) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Dave is furry.
True
4
proof
[(((((((triple3) -> rule6)) -> rule4)) -> rule3))]
("Dave" "is" "furry" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not furry.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule4)) -> rule3))]
("Dave" "is" "furry" "-")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Bob is nice.
True
5
proof
[(((((((((triple1) -> rule6)) -> rule4)) -> rule3)) -> rule7))]
("Bob" "is" "nice" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Charlie is not red.
False
9
inv-proof
[(((((((triple2) -> rule1)) -> rule7) ((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2)) -> rule5))]
("Charlie" "is" "red" "-")
((((((triple2) -> (rule1 % int4))) -> (rule7 % int3)) ((triple2 ((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is cold.
True
7
proof
[(((((((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2)) -> rule6)) -> rule4))]
("Charlie" "is" "cold" "+")
((((((triple2 ((((triple2) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
Charlie is not cold.
False
7
inv-proof
[(((((((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2)) -> rule6)) -> rule4))]
("Charlie" "is" "cold" "-")
((((((triple2 ((((triple2) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Charlie is rough.[(triple2)] Dave is blue.[(triple3)] Dave is nice.[(triple4 OR ((((((((triple3) -> rule6)) -> rule4)) -> rule3)) -> rule7))] Erin is nice.[(triple5 OR ((((triple7) -> rule1)) -> rule7))] Erin is red.[(triple6)] Erin is rough.[(triple7)] @1: Bob is kind.[(((triple1) -> rule6))] Charlie is furry.[(((triple2) -> rule1))] Dave is kind.[(((triple3) -> rule6))] Erin is blue.[(((triple7 triple5) -> rule2) OR ((triple7 ((((triple7) -> rule1)) -> rule7)) -> rule2))] Erin is furry.[(((triple7) -> rule1) OR ((((((((triple7 triple5) -> rule2)) -> rule6)) -> rule4)) -> rule3))] @2: Bob is cold.[(((((triple1) -> rule6)) -> rule4))] Charlie is nice.[(((((triple2) -> rule1)) -> rule7))] Dave is cold.[(((((triple3) -> rule6)) -> rule4))] Erin is kind.[(((((triple7 triple5) -> rule2)) -> rule6) OR ((((triple7 ((((triple7) -> rule1)) -> rule7)) -> rule2)) -> rule6))] @3: Bob is furry.[(((((((triple1) -> rule6)) -> rule4)) -> rule3))] Charlie is blue.[(((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2))] Dave is furry.[(((((((triple3) -> rule6)) -> rule4)) -> rule3))] Erin is cold.[(((((((triple7 triple5) -> rule2)) -> rule6)) -> rule4) OR ((((((triple7 ((((triple7) -> rule1)) -> rule7)) -> rule2)) -> rule6)) -> rule4))] @4: Bob is nice.[(((((((((triple1) -> rule6)) -> rule4)) -> rule3)) -> rule7))] Charlie is kind.[(((((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2)) -> rule6))] Charlie is red.[(((((((triple2) -> rule1)) -> rule7) ((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2)) -> rule5))] @5: Charlie is cold.[(((((((triple2 ((((triple2) -> rule1)) -> rule7)) -> rule2)) -> rule6)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((((((((triple3) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple7 triple5) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((triple7) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((((triple7 triple5) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple7 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple7 ((((triple7) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple7 triple5) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple7 ((((triple7) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
int5
Bob is nice.
("Bob" "is" "nice" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple2) -> (rule1 % int4))) -> (rule7 % int3)) ((triple2 ((((triple2) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2 ((((triple2) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5