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