Bob is kind. Bob is nice. Bob is red. Bob is round. Bob is young. Dave is big. Dave is red. All round things are kind. If something is big then it is round.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Bob is young.
True
1
proof
[(triple5)]
("Bob" "is" "young" "+")
triple5
Bob is not round.
False
1
inv-proof
[(triple4)]
("Bob" "is" "round" "-")
triple4
Dave is round.
True
2
proof
[(((triple6) -> rule2))]
("Dave" "is" "round" "+")
((triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple6) -> rule2))]
("Dave" "is" "round" "-")
((triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is kind.[(triple1 OR ((triple4) -> rule1))] Bob is nice.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4)] Bob is young.[(triple5)] Dave is big.[(triple6)] Dave is red.[(triple7)] @1: Dave is round.[(((triple6) -> rule2))] @2: Dave is kind.[(((((triple6) -> rule2)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((triple4) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2