Bob is big. Bob is furry. Bob is green. Bob is round. Charlie is furry. Erin is cold. Erin is furry. Erin is round. Erin is smart. Gary is furry. All smart things are green. If something is furry then it is round. Furry things are round. If something is round then it is smart. If something is cold and not furry then it is smart. Smart things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is cold and not furry then it is smart.
((("something" "is" "cold" "+") ("something" "is" "furry" "~")) -> ("something" "is" "smart" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Charlie is furry.
True
1
proof
[(triple5)]
("Charlie" "is" "furry" "+")
triple5
Erin is not smart.
False
1
inv-proof
[(triple9 OR ((triple8) -> rule4) OR ((((triple7) -> rule2)) -> rule4) OR ((((triple7) -> rule3)) -> rule4))]
("Erin" "is" "smart" "-")
triple9
((triple8) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
True
2
proof
[(((triple9) -> rule1) OR ((((triple8) -> rule4)) -> rule1) OR ((((((triple7) -> rule2)) -> rule4)) -> rule1) OR ((((((triple7) -> rule3)) -> rule4)) -> rule1))]
("Erin" "is" "green" "+")
((triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not green.
False
2
inv-proof
[(((triple9) -> rule1) OR ((((triple8) -> rule4)) -> rule1) OR ((((((triple7) -> rule2)) -> rule4)) -> rule1) OR ((((((triple7) -> rule3)) -> rule4)) -> rule1))]
("Erin" "is" "green" "-")
((triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Gary is smart.
True
3
proof
[(((((triple10) -> rule2)) -> rule4) OR ((((triple10) -> rule3)) -> rule4))]
("Gary" "is" "smart" "+")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule4) OR ((((triple10) -> rule3)) -> rule4))]
("Gary" "is" "smart" "-")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
True
4
proof
[(((((((triple10) -> rule2)) -> rule4)) -> rule1) OR ((((((triple10) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "green" "+")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not green.
False
4
inv-proof
[(((((((triple10) -> rule2)) -> rule4)) -> rule1) OR ((((((triple10) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "green" "-")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is big.[(triple1 OR ((((triple4) -> rule4)) -> rule6) OR ((((((triple2) -> rule2)) -> rule4)) -> rule6) OR ((((((triple2) -> rule3)) -> rule4)) -> rule6))] Bob is furry.[(triple2)] Bob is green.[(triple3 OR ((((triple4) -> rule4)) -> rule1) OR ((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple2) -> rule3)) -> rule4)) -> rule1))] Bob is round.[(triple4 OR ((triple2) -> rule2) OR ((triple2) -> rule3))] Charlie is furry.[(triple5)] Erin is cold.[(triple6)] Erin is furry.[(triple7)] Erin is round.[(triple8 OR ((triple7) -> rule2) OR ((triple7) -> rule3))] Erin is smart.[(triple9 OR ((triple8) -> rule4) OR ((((triple7) -> rule2)) -> rule4) OR ((((triple7) -> rule3)) -> rule4))] Gary is furry.[(triple10)] @1: Bob is smart.[(((triple4) -> rule4) OR ((((triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3)) -> rule4))] Charlie is round.[(((triple5) -> rule2) OR ((triple5) -> rule3))] Erin is big.[(((triple9) -> rule6) OR ((((triple8) -> rule4)) -> rule6) OR ((((((triple7) -> rule2)) -> rule4)) -> rule6) OR ((((((triple7) -> rule3)) -> rule4)) -> rule6))] Erin is green.[(((triple9) -> rule1) OR ((((triple8) -> rule4)) -> rule1) OR ((((((triple7) -> rule2)) -> rule4)) -> rule1) OR ((((((triple7) -> rule3)) -> rule4)) -> rule1))] Gary is round.[(((triple10) -> rule2) OR ((triple10) -> rule3))] @2: Charlie is smart.[(((((triple5) -> rule2)) -> rule4) OR ((((triple5) -> rule3)) -> rule4))] Gary is smart.[(((((triple10) -> rule2)) -> rule4) OR ((((triple10) -> rule3)) -> rule4))] @3: Charlie is big.[(((((((triple5) -> rule2)) -> rule4)) -> rule6) OR ((((((triple5) -> rule3)) -> rule4)) -> rule6))] Charlie is green.[(((((((triple5) -> rule2)) -> rule4)) -> rule1) OR ((((((triple5) -> rule3)) -> rule4)) -> rule1))] Gary is big.[(((((((triple10) -> rule2)) -> rule4)) -> rule6) OR ((((((triple10) -> rule3)) -> rule4)) -> rule6))] Gary is green.[(((((((triple10) -> rule2)) -> rule4)) -> rule1) OR ((((((triple10) -> rule3)) -> rule4)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
((triple7) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple7) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple8) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple5) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple9) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((triple10) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple10) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3