Anne is blue. Anne is quiet. Bob is big. Bob is cold. Bob is round. Dave is big. Dave is not blue. Dave is quiet. Dave is red. Dave is round. Dave is not young. Erin is big. Erin is quiet. Erin is red. Erin is round. Erin is not young. If Dave is round and Dave is blue then Dave is red. Round, cold things are not young. If something is young and not quiet then it is not cold. Red things are cold. All blue things are round. Cold, quiet things are red. All round things are red. If something is cold and not young then it is big. Red, young things are big.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not young.
("Dave" "is" "young" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not young.
("Erin" "is" "young" "-")
If Dave is round and Dave is blue then Dave is red.
((("Dave" "is" "round" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "+"))
Round, cold things are not young.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "-"))
If something is young and not quiet then it is not cold.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "cold" "-"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Cold, quiet things are red.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is cold and not young then it is big.
((("something" "is" "cold" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
Red, young things are big.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Erin is not young.
True
1
proof
[(triple16 OR ((triple15 ((triple14) -> rule4)) -> rule2) OR ((triple15 ((((triple15) -> rule7)) -> rule4)) -> rule2))]
("Erin" "is" "young" "-")
triple16
((triple15 ((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple15 ((((triple15) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Dave is not round.
False
1
inv-proof
[(triple10)]
("Dave" "is" "round" "-")
triple10
Anne is round.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "-")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule5)) -> rule7))]
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule7))]
("Anne" "is" "red" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
True
4
proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule4))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not cold.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule7)) -> rule4))]
("Anne" "is" "cold" "-")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not young.
True
7
proof
[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7)) -> rule4)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is young.
False
7
inv-proof
[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7)) -> rule4)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is big.
True
12
proof
[(((((((((triple1) -> rule5)) -> rule7)) -> rule4) ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7)) -> rule4)) -> rule2)) -> rule8))]
("Anne" "is" "big" "+")
((((((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not big.
False
12
inv-proof
[(((((((((triple1) -> rule5)) -> rule7)) -> rule4) ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7)) -> rule4)) -> rule2)) -> rule8))]
("Anne" "is" "big" "-")
((((((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2)] Bob is big.[(triple3 OR ((triple4 ((triple5 triple4) -> rule2)) -> rule8) OR ((((((triple5) -> rule7)) -> rule4) ((triple5 triple4) -> rule2)) -> rule8) OR ((triple4 ((triple5 ((((triple5) -> rule7)) -> rule4)) -> rule2)) -> rule8) OR ((((((triple5) -> rule7)) -> rule4) ((triple5 ((((triple5) -> rule7)) -> rule4)) -> rule2)) -> rule8))] Bob is cold.[(triple4 OR ((((triple5) -> rule7)) -> rule4))] Bob is round.[(triple5)] Dave is big.[(triple6 OR ((((triple9) -> rule4) triple11) -> rule8) OR ((((((triple10) -> rule7)) -> rule4) triple11) -> rule8) OR ((((triple9) -> rule4) ((triple10 ((triple9) -> rule4)) -> rule2)) -> rule8) OR ((((((triple10) -> rule7)) -> rule4) ((triple10 ((triple9) -> rule4)) -> rule2)) -> rule8) OR ((((triple9) -> rule4) ((triple10 ((((triple10) -> rule7)) -> rule4)) -> rule2)) -> rule8) OR ((((((triple10) -> rule7)) -> rule4) ((triple10 ((((triple10) -> rule7)) -> rule4)) -> rule2)) -> rule8))] Dave is not blue.[(triple7)] Dave is not young.[(triple11 OR ((triple10 ((triple9) -> rule4)) -> rule2) OR ((triple10 ((((triple10) -> rule7)) -> rule4)) -> rule2))] Dave is quiet.[(triple8)] Dave is red.[(triple9 OR ((triple10) -> rule7))] Dave is round.[(triple10)] Erin is big.[(triple12 OR ((((triple14) -> rule4) triple16) -> rule8) OR ((((((triple15) -> rule7)) -> rule4) triple16) -> rule8) OR ((((triple14) -> rule4) ((triple15 ((triple14) -> rule4)) -> rule2)) -> rule8) OR ((((((triple15) -> rule7)) -> rule4) ((triple15 ((triple14) -> rule4)) -> rule2)) -> rule8) OR ((((triple14) -> rule4) ((triple15 ((((triple15) -> rule7)) -> rule4)) -> rule2)) -> rule8) OR ((((((triple15) -> rule7)) -> rule4) ((triple15 ((((triple15) -> rule7)) -> rule4)) -> rule2)) -> rule8))] Erin is not young.[(triple16 OR ((triple15 ((triple14) -> rule4)) -> rule2) OR ((triple15 ((((triple15) -> rule7)) -> rule4)) -> rule2))] Erin is quiet.[(triple13)] Erin is red.[(triple14 OR ((triple15) -> rule7))] Erin is round.[(triple15)] @1: Anne is round.[(((triple1) -> rule5))] Bob is not young.[(((triple5 triple4) -> rule2) OR ((triple5 ((((triple5) -> rule7)) -> rule4)) -> rule2))] Bob is red.[(((triple5) -> rule7))] Dave is cold.[(((triple9) -> rule4) OR ((((triple10) -> rule7)) -> rule4))] Erin is cold.[(((triple14) -> rule4) OR ((((triple15) -> rule7)) -> rule4))] @2: Anne is red.[(((((triple1) -> rule5)) -> rule7))] @3: Anne is cold.[(((((((triple1) -> rule5)) -> rule7)) -> rule4))] @4: Anne is not young.[(((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7)) -> rule4)) -> rule2))] @5: Anne is big.[(((((((((triple1) -> rule5)) -> rule7)) -> rule4) ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule7)) -> rule4)) -> rule2)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
((triple4 ((triple5 triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not young.
("Bob" "is" "young" "-")
int2
((((((triple5) -> (rule7 % int4))) -> (rule4 % int3)) ((triple5 triple4) -> (rule2 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not young.
("Bob" "is" "young" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((triple4 ((triple5 ((((triple5) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not young.
("Bob" "is" "young" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((((triple5) -> (rule7 % int4))) -> (rule4 % int3)) ((triple5 ((((triple5) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not young.
("Bob" "is" "young" "-")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
triple4
((((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
((((triple9) -> (rule4 % int2)) triple11) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2)) triple11) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((triple9) -> (rule4 % int3)) ((triple10 ((triple9) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple10) -> (rule7 % int4))) -> (rule4 % int3)) ((triple10 ((triple9) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((triple9) -> (rule4 % int4)) ((triple10 ((((triple10) -> (rule7 % int3))) -> (rule4 % int4))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple10) -> (rule7 % int4))) -> (rule4 % int3)) ((triple10 ((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not blue.
("Dave" "is" "blue" "-")
triple7
Dave is not young.
("Dave" "is" "young" "-")
triple11
((triple10 ((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple10 ((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple10) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple12
((((triple14) -> (rule4 % int2)) triple16) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple15) -> (rule7 % int3))) -> (rule4 % int2)) triple16) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple14) -> (rule4 % int3)) ((triple15 ((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple15) -> (rule7 % int4))) -> (rule4 % int3)) ((triple15 ((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((((triple14) -> (rule4 % int4)) ((triple15 ((((triple15) -> (rule7 % int3))) -> (rule4 % int4))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
((((((triple15) -> (rule7 % int4))) -> (rule4 % int3)) ((triple15 ((((triple15) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is not young.
("Erin" "is" "young" "-")
triple16
((triple15 ((triple14) -> (rule4 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple15 ((((triple15) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple13
Erin is red.
("Erin" "is" "red" "+")
triple14
((triple15) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple15
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is not young.
("Bob" "is" "young" "-")
((triple5 triple4) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
((triple5 ((((triple5) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple9) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple14) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple15) -> (rule7 % int2))) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not young.
("Anne" "is" "young" "-")
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
((((((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5