Charlie is blue. Charlie is not cold. Charlie is nice. Charlie is white. Dave is big. Dave is blue. Dave is furry. Dave is green. Erin is furry. Erin is green. Fiona is not cold. Fiona is furry. If Erin is green then Erin is big. If someone is nice and not green then they are big. If someone is cold and big then they are not nice. If someone is cold and blue then they are not nice. If someone is cold and not big then they are furry. Big people are furry. Furry people are white. If someone is green and not furry then they are not white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
If Erin is green then Erin is big.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
If someone is nice and not green then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "big" "+"))
If someone is cold and big then they are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
If someone is cold and blue then they are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
If someone is cold and not big then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
Big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is green and not furry then they are not white.
((("someone" "is" "green" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "-"))
Charlie is nice.
True
1
proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Erin is not furry.
False
1
inv-proof
[(triple9 OR ((((triple10) -> rule1)) -> rule6))]
("Erin" "is" "furry" "-")
triple9
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is blue.[(triple1)] Charlie is nice.[(triple3)] Charlie is not cold.[(triple2)] Charlie is white.[(triple4)] Dave is big.[(triple5)] Dave is blue.[(triple6)] Dave is furry.[(triple7 OR ((triple5) -> rule6))] Dave is green.[(triple8)] Erin is furry.[(triple9 OR ((((triple10) -> rule1)) -> rule6))] Erin is green.[(triple10)] Fiona is furry.[(triple12)] Fiona is not cold.[(triple11)] @1: Dave is white.[(((triple7) -> rule7) OR ((((triple5) -> rule6)) -> rule7))] Erin is big.[(((triple10) -> rule1))] Erin is white.[(((triple9) -> rule7) OR ((((((triple10) -> rule1)) -> rule6)) -> rule7))] Fiona is white.[(((triple12) -> rule7))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
((triple5) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple10
Fiona is furry.
("Fiona" "is" "furry" "+")
triple12
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple11
Dave is white.
("Dave" "is" "white" "+")
((triple7) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((triple10) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple9) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((triple12) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1