Anne is red. Anne is rough. Anne is smart. Charlie is kind. Charlie is red. Charlie is rough. Charlie is round. Charlie is smart. Charlie is white. Charlie is young. Erin is kind. Erin is red. Erin is rough. Erin is smart. Erin is white. Erin is young. If someone is round then they are white. If Charlie is white and Charlie is red then Charlie is smart. If someone is red then they are round. White people are round. All rough people are smart. Red people are round.
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Charlie is white and Charlie is red then Charlie is smart.
((("Charlie" "is" "white" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "smart" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Charlie is rough.
True
1
proof
[(triple6)]
("Charlie" "is" "rough" "+")
triple6
Charlie is not white.
False
1
inv-proof
[(triple9 OR ((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule6)) -> rule1))]
("Charlie" "is" "white" "-")
triple9
((triple7) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is round.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule6))]
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule6))]
("Anne" "is" "round" "-")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is red.[(triple1)] Anne is rough.[(triple2)] Anne is smart.[(triple3 OR ((triple2) -> rule5))] Charlie is kind.[(triple4)] Charlie is red.[(triple5)] Charlie is rough.[(triple6)] Charlie is round.[(triple7 OR ((triple5) -> rule3) OR ((triple5) -> rule6) OR ((triple9) -> rule4))] Charlie is smart.[(triple8 OR ((triple6) -> rule5) OR ((triple9 triple5) -> rule2) OR ((((triple7) -> rule1) triple5) -> rule2) OR ((((((triple5) -> rule3)) -> rule1) triple5) -> rule2) OR ((((((triple5) -> rule6)) -> rule1) triple5) -> rule2))] Charlie is white.[(triple9 OR ((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule6)) -> rule1))] Charlie is young.[(triple10)] Erin is kind.[(triple11)] Erin is red.[(triple12)] Erin is rough.[(triple13)] Erin is smart.[(triple14 OR ((triple13) -> rule5))] Erin is white.[(triple15 OR ((((triple12) -> rule3)) -> rule1) OR ((((triple12) -> rule6)) -> rule1))] Erin is young.[(triple16)] @1: Anne is round.[(((triple1) -> rule3) OR ((triple1) -> rule6))] Erin is round.[(((triple12) -> rule3) OR ((triple12) -> rule6) OR ((triple15) -> rule4))] @2: Anne is white.[(((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule6)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((triple5) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple5) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple9) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
((triple6) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple9 triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple7) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((((triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple9
((triple7) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
Erin is smart.
("Erin" "is" "smart" "+")
triple14
((triple13) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple15
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple16
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple1) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple12) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple12) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple15) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2