Dave is big. Dave is nice. Dave is smart. Dave is white. Erin is big. Erin is round. Erin is white. Erin is young. Gary is big. Gary is young. Big people are kind. Nice, young people are big. If someone is big and nice then they are white. If Dave is young then Dave is nice. If someone is nice then they are round. All young, kind people are nice.
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is young.
("Gary" "is" "young" "+")
Big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Nice, young people are big.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is big and nice then they are white.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Dave is young then Dave is nice.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "nice" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All young, kind people are nice.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Erin is big.
True
1
proof
[(triple5)]
("Erin" "is" "big" "+")
triple5
Erin is not round.
False
1
inv-proof
[(triple6 OR ((((triple8 ((triple5) -> rule1)) -> rule6)) -> rule5))]
("Erin" "is" "round" "-")
triple6
((((triple8 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is kind.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "round" "-")
((triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is nice.
True
4
proof
[(((triple10 ((triple9) -> rule1)) -> rule6))]
("Gary" "is" "nice" "+")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((triple10 ((triple9) -> rule1)) -> rule6))]
("Gary" "is" "nice" "-")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
True
6
proof
[(((triple9 ((triple10 ((triple9) -> rule1)) -> rule6)) -> rule3))]
("Gary" "is" "white" "+")
((triple9 ((triple10 ((triple9) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not white.
False
6
inv-proof
[(((triple9 ((triple10 ((triple9) -> rule1)) -> rule6)) -> rule3))]
("Gary" "is" "white" "-")
((triple9 ((triple10 ((triple9) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Dave is big.[(triple1)] Dave is nice.[(triple2)] Dave is smart.[(triple3)] Dave is white.[(triple4 OR ((triple1 triple2) -> rule3))] Erin is big.[(triple5)] Erin is round.[(triple6 OR ((((triple8 ((triple5) -> rule1)) -> rule6)) -> rule5))] Erin is white.[(triple7 OR ((triple5 ((triple8 ((triple5) -> rule1)) -> rule6)) -> rule3))] Erin is young.[(triple8)] Gary is big.[(triple9)] Gary is young.[(triple10)] @1: Dave is kind.[(((triple1) -> rule1))] Dave is round.[(((triple2) -> rule5))] Erin is kind.[(((triple5) -> rule1))] Gary is kind.[(((triple9) -> rule1))] @2: Erin is nice.[(((triple8 ((triple5) -> rule1)) -> rule6))] Gary is nice.[(((triple10 ((triple9) -> rule1)) -> rule6))] @3: Gary is round.[(((((triple10 ((triple9) -> rule1)) -> rule6)) -> rule5))] Gary is white.[(((triple9 ((triple10 ((triple9) -> rule1)) -> rule6)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
((triple1 triple2) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((((triple8 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple5 ((triple8 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple8 ((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple10 ((triple9) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple9 ((triple10 ((triple9) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3