Bob is nice. Bob is round. Bob is smart. Bob is not young. Erin is big. Erin is nice. Erin is young. Gary is rough. Gary is smart. Gary is young. If something is rough then it is smart. All smart things are quiet. If Erin is not round then Erin is big. If something is quiet then it is nice. If something is nice and not round then it is young. If something is big and not quiet then it is young.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not young.
("Bob" "is" "young" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Erin is not round then Erin is big.
((("Erin" "is" "round" "~")) -> ("Erin" "is" "big" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not round then it is young.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "young" "+"))
If something is big and not quiet then it is young.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
Erin is big.
True
1
proof
[(triple5)]
("Erin" "is" "big" "+")
triple5
Erin is not young.
False
1
inv-proof
[(triple7)]
("Erin" "is" "young" "-")
triple7
Bob is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is nice.
True
3
proof
[(((((triple9) -> rule2)) -> rule4) OR ((((((triple8) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "nice" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not nice.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule4) OR ((((((triple8) -> rule1)) -> rule2)) -> rule4))]
("Gary" "is" "nice" "-")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is nice.[(triple1 OR ((((triple3) -> rule2)) -> rule4))] Bob is not young.[(triple4)] Bob is round.[(triple2)] Bob is smart.[(triple3)] Erin is big.[(triple5)] Erin is nice.[(triple6)] Erin is young.[(triple7)] Gary is rough.[(triple8)] Gary is smart.[(triple9 OR ((triple8) -> rule1))] Gary is young.[(triple10)] @1: Bob is quiet.[(((triple3) -> rule2))] Gary is quiet.[(((triple9) -> rule2) OR ((((triple8) -> rule1)) -> rule2))] @2: Gary is nice.[(((((triple9) -> rule2)) -> rule4) OR ((((((triple8) -> rule1)) -> rule2)) -> rule4))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not young.
("Bob" "is" "young" "-")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3