Bob is furry. Bob is not kind. Bob is not red. Bob is young. Erin is blue. Erin is kind. Erin is young. All young people are cold. If someone is green then they are cold. All furry, cold people are blue. If someone is furry and not young then they are blue. Green people are blue. Kind, blue people are furry. If Erin is blue then Erin is kind. If Bob is blue and Bob is not furry then Bob is not red.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is not red.
("Bob" "is" "red" "-")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is young.
("Erin" "is" "young" "+")
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All furry, cold people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is furry and not young then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "blue" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Kind, blue people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Erin is blue then Erin is kind.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "kind" "+"))
If Bob is blue and Bob is not furry then Bob is not red.
((("Bob" "is" "blue" "+") ("Bob" "is" "furry" "~")) -> ("Bob" "is" "red" "-"))
Erin is kind.
True
1
proof
[(triple6 OR ((triple5) -> rule7))]
("Erin" "is" "kind" "+")
triple6
((triple5) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is red.
False
1
inv-proof
[(triple3)]
("Bob" "is" "red" "+")
triple3
Erin is furry.
True
3
proof
[(((triple6 triple5) -> rule6) OR ((((triple5) -> rule7) triple5) -> rule6))]
("Erin" "is" "furry" "+")
((triple6 triple5) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple5) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not cold.
False
2
inv-proof
[(((triple7) -> rule1))]
("Erin" "is" "cold" "-")
((triple7) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Bob is blue.
True
4
proof
[(((triple1 ((triple4) -> rule1)) -> rule3))]
("Bob" "is" "blue" "+")
((triple1 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((triple1 ((triple4) -> rule1)) -> rule3))]
("Bob" "is" "blue" "-")
((triple1 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is furry.[(triple1)] Bob is not kind.[(triple2)] Bob is not red.[(triple3)] Bob is young.[(triple4)] Erin is blue.[(triple5)] Erin is kind.[(triple6 OR ((triple5) -> rule7))] Erin is young.[(triple7)] @1: Bob is cold.[(((triple4) -> rule1))] Erin is cold.[(((triple7) -> rule1))] Erin is furry.[(((triple6 triple5) -> rule6) OR ((((triple5) -> rule7) triple5) -> rule6))] @2: Bob is blue.[(((triple1 ((triple4) -> rule1)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is not kind.
("Bob" "is" "kind" "-")
triple2
Bob is not red.
("Bob" "is" "red" "-")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple5) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple7) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple6 triple5) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple5) -> (rule7 % int2)) triple5) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2