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