Anne is blue. Bob is green. Charlie is big. Charlie is blue. Charlie is green. Charlie is young. Erin is green. All blue things are rough. Big things are furry. Young, green things are smart. If something is big and rough then it is green. Furry, big things are young. All furry things are rough. All blue things are rough. If something is green and blue then it is rough.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Young, green things are smart.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is big and rough then it is green.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Furry, big things are young.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is green and blue then it is rough.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Charlie is young.
True
1
proof
[(triple6 OR ((((triple3) -> rule2) triple3) -> rule5))]
("Charlie" "is" "young" "+")
triple6
((((triple3) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not blue.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "blue" "-")
triple4
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "green" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Bob is green.[(triple2)] Charlie is big.[(triple3)] Charlie is blue.[(triple4)] Charlie is green.[(triple5 OR ((triple3 ((triple4) -> rule1)) -> rule4) OR ((triple3 ((triple4) -> rule7)) -> rule4) OR ((triple3 ((((triple3) -> rule2)) -> rule6)) -> rule4))] Charlie is young.[(triple6 OR ((((triple3) -> rule2) triple3) -> rule5))] Erin is green.[(triple7)] @1: Anne is rough.[(((triple1) -> rule1) OR ((triple1) -> rule7))] Charlie is furry.[(((triple3) -> rule2))] Charlie is rough.[(((triple4) -> rule1) OR ((triple4) -> rule7) OR ((triple5 triple4) -> rule8) OR ((((triple3) -> rule2)) -> rule6))] Charlie is smart.[(((triple6 triple5) -> rule3) OR ((triple6 ((triple3 ((triple4) -> rule1)) -> rule4)) -> rule3) OR ((triple6 ((triple3 ((triple4) -> rule7)) -> rule4)) -> rule3) OR ((((((triple3) -> rule2) triple3) -> rule5) triple5) -> rule3) OR ((((((triple3) -> rule2) triple3) -> rule5) ((triple3 ((triple4) -> rule1)) -> rule4)) -> rule3) OR ((((((triple3) -> rule2) triple3) -> rule5) ((triple3 ((triple4) -> rule7)) -> rule4)) -> rule3) OR ((triple6 ((triple3 ((((triple3) -> rule2)) -> rule6)) -> rule4)) -> rule3) OR ((((((triple3) -> rule2) triple3) -> rule5) ((triple3 ((((triple3) -> rule2)) -> rule6)) -> rule4)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
((triple3 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple3 ((triple4) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((((triple3) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 triple4) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple6 triple5) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple6 ((triple3 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((triple6 ((triple3 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple3) -> (rule2 % int3)) triple3) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple3) -> (rule2 % int5)) triple3) -> (rule5 % int4)) ((triple3 ((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
((((((triple3) -> (rule2 % int5)) triple3) -> (rule5 % int4)) ((triple3 ((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5
((triple6 ((triple3 ((((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
((((((triple3) -> (rule2 % int5)) triple3) -> (rule5 % int4)) ((triple3 ((((triple3) -> (rule2 % int5))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5