Bob is green. Bob is kind. Dave is big. Dave is green. Dave is kind. Dave is nice. Dave is young. Fiona is young. Gary is green. Gary is white. If Dave is white and Dave is big then Dave is green. If Fiona is nice and Fiona is green then Fiona is big. All white, young people are kind. Kind people are nice. Young people are rough. If Bob is nice then Bob is white. All kind people are big. Kind, big people are young.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
If Dave is white and Dave is big then Dave is green.
((("Dave" "is" "white" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "green" "+"))
If Fiona is nice and Fiona is green then Fiona is big.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "big" "+"))
All white, young people are kind.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If Bob is nice then Bob is white.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "white" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Kind, big people are young.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Gary is not white.
False
1
inv-proof
[(triple10)]
("Gary" "is" "white" "-")
triple10
Bob is nice.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "nice" "-")
((triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("Bob" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not young.
False
4
inv-proof
[(((triple2 ((triple2) -> rule7)) -> rule8))]
("Bob" "is" "young" "-")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
True
5
proof
[(((((triple2 ((triple2) -> rule7)) -> rule8)) -> rule5))]
("Bob" "is" "rough" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule7)) -> rule8)) -> rule5))]
("Bob" "is" "rough" "-")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not big.
Unknown
inv-rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule8 <- FAIL)]]
("Gary" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Dave is big.[(triple3 OR ((triple5) -> rule7))] Dave is green.[(triple4)] Dave is kind.[(triple5)] Dave is nice.[(triple6 OR ((triple5) -> rule4))] Dave is young.[(triple7 OR ((triple5 triple3) -> rule8) OR ((triple5 ((triple5) -> rule7)) -> rule8))] Fiona is young.[(triple8)] Gary is green.[(triple9)] Gary is white.[(triple10)] @1: Bob is big.[(((triple2) -> rule7))] Bob is nice.[(((triple2) -> rule4))] Dave is rough.[(((triple7) -> rule5) OR ((((triple5 triple3) -> rule8)) -> rule5) OR ((((triple5 ((triple5) -> rule7)) -> rule8)) -> rule5))] Fiona is rough.[(((triple8) -> rule5))] @2: Bob is white.[(((((triple2) -> rule4)) -> rule6))] Bob is young.[(((triple2 ((triple2) -> rule7)) -> rule8))] @3: Bob is rough.[(((((triple2 ((triple2) -> rule7)) -> rule8)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
((triple5) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
((triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple5 triple3) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple5 ((triple5) -> (rule7 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple7) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple5 triple3) -> (rule8 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple8) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3