Bob is furry. Bob is red. Bob is young. Erin is big. Erin is cold. Erin is furry. Erin is nice. Erin is red. Erin is smart. Erin is young. Fiona is cold. Fiona is furry. Fiona is nice. Fiona is red. Fiona is smart. Fiona is young. Young people are red. If Erin is smart then Erin is young. Furry people are cold. If someone is red then they are furry. If Erin is nice then Erin is big. If someone is big and smart then they are cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Erin is smart then Erin is young.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "young" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Erin is nice then Erin is big.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "big" "+"))
If someone is big and smart then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Erin is red.
True
1
proof
[(triple8 OR ((triple10) -> rule1) OR ((((triple9) -> rule2)) -> rule1))]
("Erin" "is" "red" "+")
triple8
((triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not big.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule5))]
("Erin" "is" "big" "-")
triple4
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Bob is cold.
True
2
proof
[(((triple1) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Bob" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is furry.[(triple1 OR ((triple2) -> rule4) OR ((((triple3) -> rule1)) -> rule4))] Bob is red.[(triple2 OR ((triple3) -> rule1))] Bob is young.[(triple3)] Erin is big.[(triple4 OR ((triple7) -> rule5))] Erin is cold.[(triple5 OR ((triple6) -> rule3) OR ((triple4 triple9) -> rule6) OR ((((triple8) -> rule4)) -> rule3) OR ((((triple7) -> rule5) triple9) -> rule6) OR ((((((triple10) -> rule1)) -> rule4)) -> rule3) OR ((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule3))] Erin is furry.[(triple6 OR ((triple8) -> rule4) OR ((((triple10) -> rule1)) -> rule4) OR ((((((triple9) -> rule2)) -> rule1)) -> rule4))] Erin is nice.[(triple7)] Erin is red.[(triple8 OR ((triple10) -> rule1) OR ((((triple9) -> rule2)) -> rule1))] Erin is smart.[(triple9)] Erin is young.[(triple10 OR ((triple9) -> rule2))] Fiona is cold.[(triple11 OR ((triple12) -> rule3) OR ((((triple14) -> rule4)) -> rule3) OR ((((((triple16) -> rule1)) -> rule4)) -> rule3))] Fiona is furry.[(triple12 OR ((triple14) -> rule4) OR ((((triple16) -> rule1)) -> rule4))] Fiona is nice.[(triple13)] Fiona is red.[(triple14 OR ((triple16) -> rule1))] Fiona is smart.[(triple15)] Fiona is young.[(triple16)] @1: Bob is cold.[(((triple1) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((((triple3) -> rule1)) -> rule4)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple7) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple5
((triple6) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple4 triple9) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple7) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple10) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is furry.
("Erin" "is" "furry" "+")
triple6
((triple8) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple11
((triple12) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((((triple16) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple12
((triple14) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
Fiona is red.
("Fiona" "is" "red" "+")
triple14
((triple16) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
Fiona is young.
("Fiona" "is" "young" "+")
triple16
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3