Bob is big. Bob is green. Bob is nice. Bob is round. Bob is white. Bob is not young. Dave is furry. Young people are big. Round, furry people are big. If someone is furry and not white then they are big. If Bob is not round then Bob is not big. Nice people are not young. Furry people are young. If someone is furry and big then they are green. If Dave is white and Dave is not young then Dave is green.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is not young.
("Bob" "is" "young" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Round, furry people are big.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is furry and not white then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "big" "+"))
If Bob is not round then Bob is not big.
((("Bob" "is" "round" "~")) -> ("Bob" "is" "big" "-"))
Nice people are not young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and big then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Dave is white and Dave is not young then Dave is green.
((("Dave" "is" "white" "+") ("Dave" "is" "young" "~")) -> ("Dave" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Bob is not nice.
False
1
inv-proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Dave is young.
True
2
proof
[(((triple7) -> rule6))]
("Dave" "is" "young" "+")
((triple7) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple7) -> rule6))]
("Dave" "is" "young" "-")
((triple7) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
True
3
proof
[(((((triple7) -> rule6)) -> rule1))]
("Dave" "is" "big" "+")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule1))]
("Dave" "is" "big" "-")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
True
5
proof
[(((triple7 ((((triple7) -> rule6)) -> rule1)) -> rule7))]
("Dave" "is" "green" "+")
((triple7 ((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not green.
False
5
inv-proof
[(((triple7 ((((triple7) -> rule6)) -> rule1)) -> rule7))]
("Dave" "is" "green" "-")
((triple7 ((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is not young.[(triple6 OR ((triple3) -> rule5))] Bob is round.[(triple4)] Bob is white.[(triple5)] Dave is furry.[(triple7)] @1: Dave is young.[(((triple7) -> rule6))] @2: Dave is big.[(((((triple7) -> rule6)) -> rule1))] @3: Dave is green.[(((triple7 ((((triple7) -> rule6)) -> rule1)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple6
((triple3) -> (rule5 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
((triple7) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple7 ((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3