Bob is big. Bob is not quiet. Bob is smart. Erin is cold. Erin is kind. Erin is quiet. Erin is red. Cold things are big. If Bob is not quiet then Bob is cold. If Bob is quiet then Bob is cold. If Bob is cold then Bob is furry. If something is smart and furry then it is not kind. If something is cold and not kind then it is red.
Bob is big.
("Bob" "is" "big" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Bob is not quiet then Bob is cold.
((("Bob" "is" "quiet" "~")) -> ("Bob" "is" "cold" "+"))
If Bob is quiet then Bob is cold.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "cold" "+"))
If Bob is cold then Bob is furry.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "furry" "+"))
If something is smart and furry then it is not kind.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "-"))
If something is cold and not kind then it is red.
((("something" "is" "cold" "+") ("something" "is" "kind" "~")) -> ("something" "is" "red" "+"))
Erin is quiet.
True
1
proof
[(triple6)]
("Erin" "is" "quiet" "+")
triple6
Bob is not big.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "big" "-")
triple1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is big.
True
2
proof
[(((triple4) -> rule1))]
("Erin" "is" "big" "+")
((triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("Erin" "is" "big" "-")
((triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Bob is furry.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not kind.
True
5
proof
[(((triple3 ((((triple2) -> rule2)) -> rule4)) -> rule5))]
("Bob" "is" "kind" "-")
((triple3 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is kind.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule2)) -> rule4)) -> rule5))]
("Bob" "is" "kind" "+")
((triple3 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is big.[(triple1 OR ((((triple2) -> rule2)) -> rule1))] Bob is not quiet.[(triple2)] Bob is smart.[(triple3)] Erin is cold.[(triple4)] Erin is kind.[(triple5)] Erin is quiet.[(triple6)] Erin is red.[(triple7)] @1: Bob is cold.[(((triple2) -> rule2))] Erin is big.[(((triple4) -> rule1))] @2: Bob is furry.[(((((triple2) -> rule2)) -> rule4))] @3: Bob is not kind.[(((triple3 ((((triple2) -> rule2)) -> rule4)) -> rule5))] @4: Bob is red.[(((((triple2) -> rule2) ((triple3 ((((triple2) -> rule2)) -> rule4)) -> rule5)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
((triple3 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule2 % int4)) ((triple3 ((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not kind.
("Bob" "is" "kind" "-")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4