Bob is kind. Bob is young. Erin is furry. Erin is green. Erin is red. Erin is young. Gary is furry. Gary is kind. Gary is red. Harry is big. Harry is green. Harry is red. If Bob is big and Bob is red then Bob is young. Kind people are red. All red people are young. If someone is furry then they are rough. Big people are red. Red people are furry.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
If Bob is big and Bob is red then Bob is young.
((("Bob" "is" "big" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "young" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Gary is kind.
True
1
proof
[(triple8)]
("Gary" "is" "kind" "+")
triple8
Gary is not kind.
False
1
inv-proof
[(triple8)]
("Gary" "is" "kind" "-")
triple8
Gary is young.
True
2
proof
[(((triple9) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("Gary" "is" "young" "+")
((triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not rough.
False
2
inv-proof
[(((triple7) -> rule4) OR ((((triple9) -> rule6)) -> rule4) OR ((((((triple8) -> rule2)) -> rule6)) -> rule4))]
("Gary" "is" "rough" "-")
((triple7) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Harry is rough.
True
3
proof
[(((((triple12) -> rule6)) -> rule4) OR ((((((triple10) -> rule5)) -> rule6)) -> rule4))]
("Harry" "is" "rough" "+")
((((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule4))]
("Bob" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule4))]
("Bob" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is kind.[(triple1)] Bob is young.[(triple2 OR ((((triple1) -> rule2)) -> rule3))] Erin is furry.[(triple3 OR ((triple5) -> rule6))] Erin is green.[(triple4)] Erin is red.[(triple5)] Erin is young.[(triple6 OR ((triple5) -> rule3))] Gary is furry.[(triple7 OR ((triple9) -> rule6) OR ((((triple8) -> rule2)) -> rule6))] Gary is kind.[(triple8)] Gary is red.[(triple9 OR ((triple8) -> rule2))] Harry is big.[(triple10)] Harry is green.[(triple11)] Harry is red.[(triple12 OR ((triple10) -> rule5))] @1: Bob is red.[(((triple1) -> rule2))] Erin is rough.[(((triple3) -> rule4) OR ((((triple5) -> rule6)) -> rule4))] Gary is rough.[(((triple7) -> rule4) OR ((((triple9) -> rule6)) -> rule4) OR ((((((triple8) -> rule2)) -> rule6)) -> rule4))] Gary is young.[(((triple9) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] Harry is furry.[(((triple12) -> rule6) OR ((((triple10) -> rule5)) -> rule6))] Harry is young.[(((triple12) -> rule3) OR ((((triple10) -> rule5)) -> rule3))] @2: Bob is furry.[(((((triple1) -> rule2)) -> rule6))] Harry is rough.[(((((triple12) -> rule6)) -> rule4) OR ((((((triple10) -> rule5)) -> rule6)) -> rule4))] @3: Bob is rough.[(((((((triple1) -> rule2)) -> rule6)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((triple5) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
((triple5) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple7
((triple9) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
((triple8) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((triple10) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple12) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3