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