Bob is big. Bob is green. Bob is not nice. Dave is not big. Dave is furry. Dave is not green. Dave is not kind. Dave is not nice. Dave is white. Dave is young. Fiona is big. Fiona is nice. Fiona is white. Gary is kind. Gary is nice. Gary is young. All kind, young things are white. Green, young things are kind. All green things are young. If something is green and not big then it is furry. If Fiona is not big then Fiona is green. If something is young and not kind then it is not nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Dave is not big.
("Dave" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
All kind, young things are white.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Green, young things are kind.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is green and not big then it is furry.
((("something" "is" "green" "+") ("something" "is" "big" "~")) -> ("something" "is" "furry" "+"))
If Fiona is not big then Fiona is green.
((("Fiona" "is" "big" "~")) -> ("Fiona" "is" "green" "+"))
If something is young and not kind then it is not nice.
((("something" "is" "young" "+") ("something" "is" "kind" "~")) -> ("something" "is" "nice" "-"))
Gary is nice.
True
1
proof
[(triple15)]
("Gary" "is" "nice" "+")
triple15
Dave is kind.
False
1
inv-proof
[(triple7)]
("Dave" "is" "kind" "+")
triple7
Bob is young.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "young" "-")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Bob" "is" "kind" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not kind.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule2))]
("Bob" "is" "kind" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
True
7
proof
[(((((triple2 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "white" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not white.
False
7
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "white" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "furry" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
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 green.[(triple2)] Bob is not nice.[(triple3)] Dave is furry.[(triple5)] Dave is not big.[(triple4)] Dave is not green.[(triple6)] Dave is not kind.[(triple7)] Dave is not nice.[(triple8 OR ((triple10 triple7) -> rule6))] Dave is white.[(triple9)] Dave is young.[(triple10)] Fiona is big.[(triple11)] Fiona is nice.[(triple12)] Fiona is white.[(triple13)] Gary is kind.[(triple14)] Gary is nice.[(triple15)] Gary is young.[(triple16)] @1: Bob is young.[(((triple2) -> rule3))] Gary is white.[(((triple14 triple16) -> rule1))] @2: Bob is kind.[(((triple2 ((triple2) -> rule3)) -> rule2))] @3: Bob is white.[(((((triple2 ((triple2) -> rule3)) -> rule2) ((triple2) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is not big.
("Dave" "is" "big" "-")
triple4
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is not kind.
("Dave" "is" "kind" "-")
triple7
Dave is not nice.
("Dave" "is" "nice" "-")
triple8
((triple10 triple7) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is white.
("Fiona" "is" "white" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple14 triple16) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) ((triple2) -> (rule3 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3