Charlie is big. Charlie is green. Charlie is red. Charlie is round. Charlie is young. Erin is big. Erin is cold. Erin is green. Erin is nice. Erin is not red. Erin is round. Erin is not young. Gary is big. Gary is green. Gary is nice. Gary is red. Big things are round. If something is big then it is round. All green, big things are round. If Erin is green then Erin is nice. All red things are big. Round things are big. If something is cold and not green then it is not red. If something is cold then it is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is not young.
("Erin" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All green, big things are round.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Erin is green then Erin is nice.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "nice" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is cold and not green then it is not red.
((("something" "is" "cold" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "-"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Gary is green.
True
1
proof
[(triple14)]
("Gary" "is" "green" "+")
triple14
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule5) OR ((triple4) -> rule6))]
("Charlie" "is" "big" "-")
triple1
((triple3) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "nice" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Charlie is big.[(triple1 OR ((triple3) -> rule5) OR ((triple4) -> rule6))] Charlie is green.[(triple2)] Charlie is red.[(triple3)] Charlie is round.[(triple4 OR ((triple1) -> rule1) OR ((triple1) -> rule2) OR ((triple2 triple1) -> rule3) OR ((((triple3) -> rule5)) -> rule1) OR ((((triple3) -> rule5)) -> rule2) OR ((triple2 ((triple3) -> rule5)) -> rule3))] Charlie is young.[(triple5)] Erin is big.[(triple6 OR ((triple11) -> rule6))] Erin is cold.[(triple7)] Erin is green.[(triple8)] Erin is nice.[(triple9 OR ((triple7) -> rule8) OR ((triple8) -> rule4))] Erin is not red.[(triple10)] Erin is not young.[(triple12)] Erin is round.[(triple11 OR ((triple6) -> rule1) OR ((triple6) -> rule2) OR ((triple8 triple6) -> rule3))] Gary is big.[(triple13 OR ((triple16) -> rule5))] Gary is green.[(triple14)] Gary is nice.[(triple15)] Gary is red.[(triple16)] @1: Gary is round.[(((triple13) -> rule1) OR ((triple13) -> rule2) OR ((triple14 triple13) -> rule3) OR ((((triple16) -> rule5)) -> rule1) OR ((((triple16) -> rule5)) -> rule2) OR ((triple14 ((triple16) -> rule5)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple4) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple2 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
((triple11) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple7) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple8) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
triple10
Erin is not young.
("Erin" "is" "young" "-")
triple12
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple6) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple6) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple8 triple6) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple13
((triple16) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is red.
("Gary" "is" "red" "+")
triple16
Gary is round.
("Gary" "is" "round" "+")
((triple13) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple13) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple14 triple13) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple16) -> (rule5 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple16) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple14 ((triple16) -> (rule5 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2