Bob is big. Bob is blue. Bob is green. Bob is round. Bob is smart. Gary is green. Gary is smart. If someone is round then they are young. If someone is kind and round then they are not young. If someone is big and round then they are young. If someone is big and kind then they are blue. If someone is smart then they are green. Big, young people are smart. All young people are not kind. If Gary is green then Gary is young.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and round then they are not young.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
If someone is big and round then they are young.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is big and kind then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Big, young people are smart.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All young people are not kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
If Gary is green then Gary is young.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "young" "+"))
Bob is blue.
True
1
proof
[(triple2)]
("Bob" "is" "blue" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple4)]
("Bob" "is" "round" "-")
triple4
Gary is young.
True
2
proof
[(((triple6) -> rule8) OR ((((triple7) -> rule5)) -> rule8))]
("Gary" "is" "young" "+")
((triple6) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Bob is not young.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple1 triple4) -> rule3))]
("Bob" "is" "young" "-")
((triple4) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple1 triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not kind.
True
3
proof
[(((((triple4) -> rule1)) -> rule7) OR ((((triple1 triple4) -> rule3)) -> rule7))]
("Bob" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is kind.
False
3
inv-proof
[(((((triple6) -> rule8)) -> rule7) OR ((((((triple7) -> rule5)) -> rule8)) -> rule7))]
("Gary" "is" "kind" "+")
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is green.[(triple3 OR ((triple5) -> rule5) OR ((((triple1 ((triple4) -> rule1)) -> rule6)) -> rule5) OR ((((triple1 ((triple1 triple4) -> rule3)) -> rule6)) -> rule5))] Bob is round.[(triple4)] Bob is smart.[(triple5 OR ((triple1 ((triple4) -> rule1)) -> rule6) OR ((triple1 ((triple1 triple4) -> rule3)) -> rule6))] Gary is green.[(triple6 OR ((triple7) -> rule5))] Gary is smart.[(triple7)] @1: Bob is young.[(((triple4) -> rule1) OR ((triple1 triple4) -> rule3))] Gary is young.[(((triple6) -> rule8) OR ((((triple7) -> rule5)) -> rule8))] @2: Bob is not kind.[(((((triple4) -> rule1)) -> rule7) OR ((((triple1 triple4) -> rule3)) -> rule7))] Gary is not kind.[(((((triple6) -> rule8)) -> rule7) OR ((((((triple7) -> rule5)) -> rule8)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple5) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple1 ((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple1 ((triple1 triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple1 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple1 ((triple1 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple4) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple1 triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple6) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple7) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3