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