Bob is nice. Bob is rough. Erin is quiet. Erin is red. Erin is rough. Erin is white. Erin is young. Red things are white. If Bob is white then Bob is blue. All nice things are young. Nice, red things are young. If something is quiet and not nice then it is not young. All quiet things are red. If something is nice and rough then it is quiet. All blue things are quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Bob is white then Bob is blue.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "blue" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Nice, red things are young.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is quiet and not nice then it is not young.
((("something" "is" "quiet" "+") ("something" "is" "nice" "~")) -> ("something" "is" "young" "-"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is nice and rough then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule6))]
("Erin" "is" "red" "-")
triple4
((triple3) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Bob is quiet.
True
3
proof
[(((triple1 triple2) -> rule7))]
("Bob" "is" "quiet" "+")
((triple1 triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
3
inv-proof
[(((triple1 triple2) -> rule7))]
("Bob" "is" "quiet" "-")
((triple1 triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
True
4
proof
[(((((triple1 triple2) -> rule7)) -> rule6))]
("Bob" "is" "red" "+")
((((triple1 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not red.
False
4
inv-proof
[(((((triple1 triple2) -> rule7)) -> rule6))]
("Bob" "is" "red" "-")
((((triple1 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
True
5
proof
[(((((((triple1 triple2) -> rule7)) -> rule6)) -> rule1))]
("Bob" "is" "white" "+")
((((((triple1 triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not white.
False
5
inv-proof
[(((((((triple1 triple2) -> rule7)) -> rule6)) -> rule1))]
("Bob" "is" "white" "-")
((((((triple1 triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is nice.[(triple1)] Bob is rough.[(triple2)] Erin is quiet.[(triple3)] Erin is red.[(triple4 OR ((triple3) -> rule6))] Erin is rough.[(triple5)] Erin is white.[(triple6 OR ((triple4) -> rule1) OR ((((triple3) -> rule6)) -> rule1))] Erin is young.[(triple7)] @1: Bob is quiet.[(((triple1 triple2) -> rule7))] Bob is young.[(((triple1) -> rule3) OR ((triple1 ((((triple1 triple2) -> rule7)) -> rule6)) -> rule4))] @2: Bob is red.[(((((triple1 triple2) -> rule7)) -> rule6))] @3: Bob is white.[(((((((triple1 triple2) -> rule7)) -> rule6)) -> rule1))] @4: Bob is blue.[(((((((((triple1 triple2) -> rule7)) -> rule6)) -> rule1)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple3) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple4) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1 triple2) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple1 ((((triple1 triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple1 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1 triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((((((triple1 triple2) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4