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