Anne is big. Anne is green. Anne is nice. Anne is white. Dave is green. Dave is rough. Harry is rough. If Harry is big then Harry is smart. If Harry is big and Harry is smart then Harry is nice. White, nice things are blue. If something is blue and white then it is rough. If Anne is white then Anne is blue. All rough things are big. Nice, white things are green. If something is white then it is rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is big then Harry is smart.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "smart" "+"))
If Harry is big and Harry is smart then Harry is nice.
((("Harry" "is" "big" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "nice" "+"))
White, nice things are blue.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is blue and white then it is rough.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Anne is white then Anne is blue.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "blue" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Nice, white things are green.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple6)]
("Dave" "is" "rough" "+")
triple6
Anne is not white.
False
1
inv-proof
[(triple4)]
("Anne" "is" "white" "-")
triple4
Anne is blue.
True
2
proof
[(((triple4) -> rule5) OR ((triple4 triple3) -> rule3))]
("Anne" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple4 triple3) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple7) -> rule6))]
("Harry" "is" "big" "-")
((triple7) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
True
3
proof
[(((((triple7) -> rule6)) -> rule1))]
("Harry" "is" "smart" "+")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule1))]
("Harry" "is" "smart" "-")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "green" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((((triple4) -> rule8)) -> rule6) OR ((((((triple4) -> rule5) triple4) -> rule4)) -> rule6) OR ((((((triple4 triple3) -> rule3) triple4) -> rule4)) -> rule6))] Anne is green.[(triple2 OR ((triple3 triple4) -> rule7))] Anne is nice.[(triple3)] Anne is white.[(triple4)] Dave is green.[(triple5)] Dave is rough.[(triple6)] Harry is rough.[(triple7)] @1: Anne is blue.[(((triple4) -> rule5) OR ((triple4 triple3) -> rule3))] Anne is rough.[(((triple4) -> rule8) OR ((((triple4) -> rule5) triple4) -> rule4) OR ((((triple4 triple3) -> rule3) triple4) -> rule4))] Dave is big.[(((triple6) -> rule6))] Harry is big.[(((triple7) -> rule6))] @2: Harry is smart.[(((((triple7) -> rule6)) -> rule1))] @3: Harry is nice.[(((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((((triple4) -> (rule5 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple4 triple3) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3 triple4) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple4 triple3) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple4) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple4) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple4 triple3) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple6) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7) -> (rule6 % int3)) ((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3