Bob is nice. Dave is big. Dave is smart. Fiona is smart. Gary is furry. Gary is nice. Gary is young. If something is young then it is big. All young things are nice. If Gary is quiet then Gary is nice. All young things are big. If something is big and nice then it is smart. If Gary is kind then Gary is nice.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Gary is quiet then Gary is nice.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is big and nice then it is smart.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Gary is kind then Gary is nice.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "nice" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is nice.[(triple1)] Dave is big.[(triple2)] Dave is smart.[(triple3)] Fiona is smart.[(triple4)] Gary is furry.[(triple5)] Gary is nice.[(triple6 OR ((triple7) -> rule2))] Gary is young.[(triple7)] @1: Gary is big.[(((triple7) -> rule1) OR ((triple7) -> rule4))] @2: Gary is smart.[(((((triple7) -> rule1) triple6) -> rule5) OR ((((triple7) -> rule4) triple6) -> rule5) OR ((((triple7) -> rule1) ((triple7) -> rule2)) -> rule5) OR ((((triple7) -> rule4) ((triple7) -> rule2)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
((triple7) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
((triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple7) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple7) -> (rule1 % int2)) triple6) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple7) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((triple7) -> (rule4 % int3)) ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3