Anne is big. Anne is nice. Anne is red. Anne is round. Bob is big. Bob is kind. Bob is nice. Bob is round. Harry is big. Harry is kind. Harry is nice. Harry is red. Harry is rough. Harry is round. Harry is young. Nice, round things are young. If Harry is rough then Harry is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Nice, round things are young.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If Harry is rough then Harry is round.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Anne is not round.
False
1
inv-proof
[(triple4)]
("Anne" "is" "round" "-")
triple4
Bob is young.
True
3
proof
[(((triple7 triple8) -> rule1))]
("Bob" "is" "young" "+")
((triple7 triple8) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is not young.
False
3
inv-proof
[(((triple2 triple4) -> rule1))]
("Anne" "is" "young" "-")
((triple2 triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Anne is red.[(triple3)] Anne is round.[(triple4)] Bob is big.[(triple5)] Bob is kind.[(triple6)] Bob is nice.[(triple7)] Bob is round.[(triple8)] Harry is big.[(triple9)] Harry is kind.[(triple10)] Harry is nice.[(triple11)] Harry is red.[(triple12)] Harry is rough.[(triple13)] Harry is round.[(triple14 OR ((triple13) -> rule2))] Harry is young.[(triple15 OR ((triple11 triple14) -> rule1) OR ((triple11 ((triple13) -> rule2)) -> rule1))] @1: Anne is young.[(((triple2 triple4) -> rule1))] Bob is young.[(((triple7 triple8) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple13) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple11 triple14) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple11 ((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple2 triple4) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple7 triple8) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1