Charlie is nice. Erin is nice. Erin is red. Fiona is big. Fiona is green. Fiona is red. Fiona is smart. If something is big and nice then it is red. Nice, furry things are red. Smart, nice things are big. All red things are green. All nice things are smart. All red things are big. If something is big and nice then it is red. If Charlie is red then Charlie is green.
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is big and nice then it is red.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Nice, furry things are red.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Smart, nice things are big.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is big and nice then it is red.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Charlie is red then Charlie is green.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple3 OR ((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule1) OR ((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule7))]
("Erin" "is" "red" "+")
triple3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is not smart.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "smart" "-")
triple7
Erin is green.
True
2
proof
[(((triple3) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule1)) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule7)) -> rule4))]
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule1)) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule7)) -> rule4))]
("Erin" "is" "green" "-")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Charlie is big.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not big.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule3))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is red.
True
6
proof
[(((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule1) OR ((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule7))]
("Charlie" "is" "red" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not red.
False
6
inv-proof
[(((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule1) OR ((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule7))]
("Charlie" "is" "red" "-")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is nice.[(triple1)] Erin is nice.[(triple2)] Erin is red.[(triple3 OR ((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule1) OR ((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule7))] Fiona is big.[(triple4 OR ((triple6) -> rule6))] Fiona is green.[(triple5 OR ((triple6) -> rule4))] Fiona is red.[(triple6)] Fiona is smart.[(triple7)] @1: Charlie is smart.[(((triple1) -> rule5))] Erin is big.[(((triple3) -> rule6) OR ((((triple2) -> rule5) triple2) -> rule3))] Erin is green.[(((triple3) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule1)) -> rule4) OR ((((((((triple2) -> rule5) triple2) -> rule3) triple2) -> rule7)) -> rule4))] Erin is smart.[(((triple2) -> rule5))] @2: Charlie is big.[(((((triple1) -> rule5) triple1) -> rule3))] @3: Charlie is red.[(((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule1) OR ((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule7))] @4: Charlie is green.[(((((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule1)) -> rule4) OR ((((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule1)) -> rule8) OR ((((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule7)) -> rule4) OR ((((((((triple1) -> rule5) triple1) -> rule3) triple1) -> rule7)) -> rule8))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
((triple6) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple5
((triple6) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((((((((triple2) -> (rule5 % int4)) triple2) -> (rule3 % int3)) triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3)) triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3)) triple1) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4