Anne is big. Anne is blue. Anne is cold. Anne is nice. Anne is rough. Anne is smart. Anne is white. Dave is big. Dave is cold. Dave is smart. Dave is white. Erin is big. Erin is blue. Erin is cold. Erin is nice. Erin is rough. If Erin is white and Erin is big then Erin is not smart. If Erin is white and Erin is rough then Erin is smart. Cold, smart things are blue. All big things are blue. Nice, big things are rough. All white, nice things are smart. All big, smart things are nice. Nice things are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If Erin is white and Erin is big then Erin is not smart.
((("Erin" "is" "white" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "smart" "-"))
If Erin is white and Erin is rough then Erin is smart.
((("Erin" "is" "white" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
Cold, smart things are blue.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Nice, big things are rough.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All white, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All big, smart things are nice.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Anne is cold.
True
1
proof
[(triple3)]
("Anne" "is" "cold" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple11)]
("Dave" "is" "white" "-")
triple11
Dave is blue.
True
2
proof
[(((triple8) -> rule4) OR ((triple9 triple10) -> rule3))]
("Dave" "is" "blue" "+")
((triple8) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple9 triple10) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple8) -> rule4) OR ((triple9 triple10) -> rule3))]
("Dave" "is" "blue" "-")
((triple8) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple9 triple10) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
True
5
proof
[(((((triple8 triple10) -> rule7) triple8) -> rule5))]
("Dave" "is" "rough" "+")
((((triple8 triple10) -> (rule7 % int2)) triple8) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not rough.
False
5
inv-proof
[(((((triple8 triple10) -> rule7) triple8) -> rule5))]
("Dave" "is" "rough" "-")
((((triple8 triple10) -> (rule7 % int2)) triple8) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is big.[(triple1 OR ((triple4) -> rule8))] Anne is blue.[(triple2 OR ((triple1) -> rule4) OR ((triple3 triple6) -> rule3) OR ((((triple4) -> rule8)) -> rule4) OR ((triple3 ((triple7 triple4) -> rule6)) -> rule3))] Anne is cold.[(triple3)] Anne is nice.[(triple4 OR ((triple1 triple6) -> rule7))] Anne is rough.[(triple5 OR ((triple4 triple1) -> rule5) OR ((triple4 ((triple4) -> rule8)) -> rule5) OR ((((triple1 triple6) -> rule7) triple1) -> rule5) OR ((((triple1 triple6) -> rule7) ((triple4) -> rule8)) -> rule5))] Anne is smart.[(triple6 OR ((triple7 triple4) -> rule6))] Anne is white.[(triple7)] Dave is big.[(triple8)] Dave is cold.[(triple9)] Dave is smart.[(triple10)] Dave is white.[(triple11)] Erin is big.[(triple12 OR ((triple15) -> rule8))] Erin is blue.[(triple13 OR ((triple12) -> rule4) OR ((((triple15) -> rule8)) -> rule4))] Erin is cold.[(triple14)] Erin is nice.[(triple15)] Erin is rough.[(triple16 OR ((triple15 triple12) -> rule5) OR ((triple15 ((triple15) -> rule8)) -> rule5))] @1: Dave is blue.[(((triple8) -> rule4) OR ((triple9 triple10) -> rule3))] Dave is nice.[(((triple8 triple10) -> rule7))] @2: Dave is rough.[(((((triple8 triple10) -> rule7) triple8) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple3 triple6) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((triple3 ((triple7 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple1 triple6) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple4 triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 ((triple4) -> (rule8 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1 triple6) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple1 triple6) -> (rule7 % int3)) ((triple4) -> (rule8 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple7 triple4) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
((triple15) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple13
((triple12) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple15) -> (rule8 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple14
Erin is nice.
("Erin" "is" "nice" "+")
triple15
Erin is rough.
("Erin" "is" "rough" "+")
triple16
((triple15 triple12) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple15 ((triple15) -> (rule8 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple8) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple9 triple10) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple8 triple10) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple8 triple10) -> (rule7 % int2)) triple8) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2