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