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