Dave is smart. Fiona is nice. Big people are quiet. Nice people are big. If someone is big and not furry then they are green. If Fiona is smart and Fiona is big then Fiona is young. All quiet people are young. If someone is smart and not green then they are young.
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is big and not furry then they are green.
((("someone" "is" "big" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "+"))
If Fiona is smart and Fiona is big then Fiona is young.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "big" "+")) -> ("Fiona" "is" "young" "+"))
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is smart and not green then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "young" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Fiona is big.
True
2
proof
[(((triple2) -> rule2))]
("Fiona" "is" "big" "+")
((triple2) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Fiona" "is" "big" "-")
((triple2) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule5))]
("Fiona" "is" "young" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule5))]
("Fiona" "is" "young" "-")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "quiet" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Dave is smart.[(triple1)] Fiona is nice.[(triple2)] @1: Fiona is big.[(((triple2) -> rule2))] @2: Fiona is quiet.[(((((triple2) -> rule2)) -> rule1))] @3: Fiona is young.[(((((((triple2) -> rule2)) -> rule1)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
((triple2) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3