Anne is big. Anne is green. Anne is nice. Anne is smart. Anne is young. Dave is furry. Erin is nice. Erin is round. Erin is smart. Fiona is big. Fiona is furry. Fiona is smart. Smart, nice things are green. Green, big things are young. If something is young then it is nice. Green things are round. All big things are green. If something is nice and smart then it is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart, nice things are green.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Green, big things are young.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is nice and smart then it is young.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Anne is green.
True
1
proof
[(triple2 OR ((triple1) -> rule5) OR ((triple4 triple3) -> rule1) OR ((triple4 ((triple5) -> rule3)) -> rule1))]
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not young.
False
1
inv-proof
[(triple5 OR ((triple2 triple1) -> rule2) OR ((triple3 triple4) -> rule6) OR ((((triple1) -> rule5) triple1) -> rule2) OR ((((triple4 triple3) -> rule1) triple1) -> rule2))]
("Anne" "is" "young" "-")
triple5
((triple2 triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3 triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4 triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is green.
True
3
proof
[(((triple9 triple7) -> rule1))]
("Erin" "is" "green" "+")
((triple9 triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
3
inv-proof
[(((triple9 triple7) -> rule1))]
("Erin" "is" "green" "-")
((triple9 triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule5) OR ((triple4 triple3) -> rule1) OR ((triple4 ((triple5) -> rule3)) -> rule1))] Anne is nice.[(triple3 OR ((triple5) -> rule3) OR ((((triple2 triple1) -> rule2)) -> rule3) OR ((((((triple1) -> rule5) triple1) -> rule2)) -> rule3))] Anne is smart.[(triple4)] Anne is young.[(triple5 OR ((triple2 triple1) -> rule2) OR ((triple3 triple4) -> rule6) OR ((((triple1) -> rule5) triple1) -> rule2) OR ((((triple4 triple3) -> rule1) triple1) -> rule2))] Dave is furry.[(triple6)] Erin is nice.[(triple7)] Erin is round.[(triple8 OR ((((triple9 triple7) -> rule1)) -> rule4))] Erin is smart.[(triple9)] Fiona is big.[(triple10)] Fiona is furry.[(triple11)] Fiona is smart.[(triple12)] @1: Anne is round.[(((triple2) -> rule4) OR ((((triple1) -> rule5)) -> rule4) OR ((((triple4 triple3) -> rule1)) -> rule4) OR ((((triple4 ((triple5) -> rule3)) -> rule1)) -> rule4))] Erin is green.[(((triple9 triple7) -> rule1))] Erin is young.[(((triple7 triple9) -> rule6))] Fiona is green.[(((triple10) -> rule5))] @2: Fiona is round.[(((((triple10) -> rule5)) -> rule4))] Fiona is young.[(((((triple10) -> rule5) triple10) -> rule2))] @3: Fiona is nice.[(((((((triple10) -> rule5) triple10) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple4 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple5) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple2 triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((((triple1) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple2 triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3 triple4) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4 triple3) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
triple8
((((triple9 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Fiona is big.
("Fiona" "is" "big" "+")
triple10
Fiona is furry.
("Fiona" "is" "furry" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple9 triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple7 triple9) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple10) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple10) -> (rule5 % int2)) triple10) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((triple10) -> (rule5 % int3)) triple10) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3