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