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