Anne is big. Anne is nice. Anne is young. Charlie is nice. Charlie is red. Charlie is smart. Erin is blue. Blue things are young. Nice things are young. All young, red things are nice. All young things are smart. Blue things are smart. Young things are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All young, red things are nice.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Charlie is red.
True
1
proof
[(triple5 OR ((((triple4) -> rule2)) -> rule6))]
("Charlie" "is" "red" "+")
triple5
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Anne is not young.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule2))]
("Anne" "is" "young" "-")
triple3
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
True
2
proof
[(((triple3) -> rule4) OR ((((triple2) -> rule2)) -> rule4))]
("Anne" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not smart.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((triple2) -> rule2)) -> rule4))]
("Anne" "is" "smart" "-")
((triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is red.
True
3
proof
[(((((triple7) -> rule1)) -> rule6))]
("Erin" "is" "red" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule6))]
("Erin" "is" "red" "-")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
True
6
proof
[(((((triple7) -> rule1) ((((triple7) -> rule1)) -> rule6)) -> rule3))]
("Erin" "is" "nice" "+")
((((triple7) -> (rule1 % int3)) ((((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not nice.
False
6
inv-proof
[(((((triple7) -> rule1) ((((triple7) -> rule1)) -> rule6)) -> rule3))]
("Erin" "is" "nice" "-")
((((triple7) -> (rule1 % int3)) ((((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2 OR ((triple3 ((triple3) -> rule6)) -> rule3))] Anne is young.[(triple3 OR ((triple2) -> rule2))] Charlie is nice.[(triple4)] Charlie is red.[(triple5 OR ((((triple4) -> rule2)) -> rule6))] Charlie is smart.[(triple6 OR ((((triple4) -> rule2)) -> rule4))] Erin is blue.[(triple7)] @1: Anne is red.[(((triple3) -> rule6) OR ((((triple2) -> rule2)) -> rule6))] Anne is smart.[(((triple3) -> rule4) OR ((((triple2) -> rule2)) -> rule4))] Charlie is young.[(((triple4) -> rule2))] Erin is smart.[(((triple7) -> rule5) OR ((((triple7) -> rule1)) -> rule4))] Erin is young.[(((triple7) -> rule1))] @2: Erin is red.[(((((triple7) -> rule1)) -> rule6))] @3: Erin is nice.[(((((triple7) -> rule1) ((((triple7) -> rule1)) -> rule6)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple3) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple4) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple7) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple7) -> (rule1 % int3)) ((((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3