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