Anne is blue. Anne is cold. Anne is smart. Gary is big. Gary is cold. Gary is white. Harry is rough. Big, smart people are young. If Harry is young then Harry is blue. If Harry is big and Harry is smart then Harry is rough. Big people are rough. Blue, smart people are big. If someone is blue then they are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Big, smart people are young.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If Harry is young then Harry is blue.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is big and Harry is smart then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Blue, smart people are big.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Harry is not rough.
False
1
inv-proof
[(triple7)]
("Harry" "is" "rough" "-")
triple7
Gary is rough.
True
2
proof
[(((triple4) -> rule4))]
("Gary" "is" "rough" "+")
((triple4) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is not big.
False
3
inv-proof
[(((triple1 triple3) -> rule5) OR ((triple1 ((triple1) -> rule6)) -> rule5))]
("Anne" "is" "big" "-")
((triple1 triple3) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is big.
Unknown
rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- FAIL)]]
("Harry" "is" "big" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is smart.[(triple3 OR ((triple1) -> rule6))] Gary is big.[(triple4)] Gary is cold.[(triple5)] Gary is white.[(triple6)] Harry is rough.[(triple7)] @1: Anne is big.[(((triple1 triple3) -> rule5) OR ((triple1 ((triple1) -> rule6)) -> rule5))] Gary is rough.[(((triple4) -> rule4))] @2: Anne is rough.[(((((triple1 triple3) -> rule5)) -> rule4) OR ((((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4))] Anne is young.[(((((triple1 triple3) -> rule5) triple3) -> rule1) OR ((((triple1 triple3) -> rule5) ((triple1) -> rule6)) -> rule1) OR ((((triple1 ((triple1) -> rule6)) -> rule5) triple3) -> rule1) OR ((((triple1 ((triple1) -> rule6)) -> rule5) ((triple1) -> rule6)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1 triple3) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((triple1 triple3) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1 triple3) -> (rule5 % int3)) ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule6 % int3))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3