Bob is not quiet. Dave is red. Erin is not quiet. If Erin is not quiet then Erin is nice. All nice people are not big.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
If Erin is not quiet then Erin is nice.
((("Erin" "is" "quiet" "~")) -> ("Erin" "is" "nice" "+"))
All nice people are not big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "-"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Bob is quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Erin is nice.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not big.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is not quiet.[(triple1)] Dave is red.[(triple2)] Erin is not quiet.[(triple3)] @1: Erin is nice.[(((triple3) -> rule1))] @2: Erin is not big.[(((((triple3) -> rule1)) -> rule2))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not big.
("Erin" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2