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