Bob is rough. Bob is not young. Dave is big. Dave is nice. Dave is quiet. Dave is rough. Fiona is cold. Fiona is nice. Fiona is quiet. Gary is big. Gary is white. Gary is young. If someone is quiet and not big then they are not nice. If someone is white and big then they are nice. If someone is white and cold then they are not rough. All nice people are cold. If someone is nice and not quiet then they are white. If someone is quiet and not cold then they are not young.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not young.
("Bob" "is" "young" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is quiet and not big then they are not nice.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "nice" "-"))
If someone is white and big then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and cold then they are not rough.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "-"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and not quiet then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "white" "+"))
If someone is quiet and not cold then they are not young.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "young" "-"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Fiona is not quiet.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "quiet" "-")
triple9
Gary is nice.
True
3
proof
[(((triple11 triple10) -> rule2))]
("Gary" "is" "nice" "+")
((triple11 triple10) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple4) -> rule4))]
("Dave" "is" "cold" "-")
((triple4) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is cold.
True
4
proof
[(((((triple11 triple10) -> rule2)) -> rule4))]
("Gary" "is" "cold" "+")
((((triple11 triple10) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not cold.
False
4
inv-proof
[(((((triple11 triple10) -> rule2)) -> rule4))]
("Gary" "is" "cold" "-")
((((triple11 triple10) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not rough.
True
6
proof
[(((triple11 ((((triple11 triple10) -> rule2)) -> rule4)) -> rule3))]
("Gary" "is" "rough" "-")
((triple11 ((((triple11 triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is rough.
False
6
inv-proof
[(((triple11 ((((triple11 triple10) -> rule2)) -> rule4)) -> rule3))]
("Gary" "is" "rough" "+")
((triple11 ((((triple11 triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Bob is not young.[(triple2)] Bob is rough.[(triple1)] Dave is big.[(triple3)] Dave is nice.[(triple4)] Dave is quiet.[(triple5)] Dave is rough.[(triple6)] Fiona is cold.[(triple7 OR ((triple8) -> rule4))] Fiona is nice.[(triple8)] Fiona is quiet.[(triple9)] Gary is big.[(triple10)] Gary is white.[(triple11)] Gary is young.[(triple12)] @1: Dave is cold.[(((triple4) -> rule4))] Gary is nice.[(((triple11 triple10) -> rule2))] @2: Gary is cold.[(((((triple11 triple10) -> rule2)) -> rule4))] @3: Gary is not rough.[(((triple11 ((((triple11 triple10) -> rule2)) -> rule4)) -> rule3))]
Bob is not young.
("Bob" "is" "young" "-")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
((triple8) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple11 triple10) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple11 triple10) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not rough.
("Gary" "is" "rough" "-")
((triple11 ((((triple11 triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3