Charlie is big. Erin is young. Fiona is rough. Gary is nice. Gary is rough. Gary is smart. Gary is young. Rough people are quiet. If Gary is young then Gary is big. Big, furry people are rough. If Gary is furry then Gary is quiet. All nice, quiet people are big. Nice people are rough. If someone is smart and nice then they are big. All young, big people are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is young then Gary is big.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "big" "+"))
Big, furry people are rough.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Gary is furry then Gary is quiet.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "quiet" "+"))
All nice, quiet people are big.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and nice then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All young, big people are smart.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Fiona is rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple7)]
("Gary" "is" "young" "-")
triple7
Gary is big.
True
2
proof
[(((triple7) -> rule2) OR ((triple6 triple4) -> rule7) OR ((triple4 ((triple5) -> rule1)) -> rule5) OR ((triple4 ((((triple4) -> rule6)) -> rule1)) -> rule5))]
("Gary" "is" "big" "+")
((triple7) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6 triple4) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple4 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple4 ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Fiona is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Fiona" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "rough" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is big.[(triple1)] Erin is young.[(triple2)] Fiona is rough.[(triple3)] Gary is nice.[(triple4)] Gary is rough.[(triple5 OR ((triple4) -> rule6))] Gary is smart.[(triple6 OR ((triple7 ((triple7) -> rule2)) -> rule8) OR ((triple7 ((triple4 ((triple5) -> rule1)) -> rule5)) -> rule8) OR ((triple7 ((triple4 ((((triple4) -> rule6)) -> rule1)) -> rule5)) -> rule8))] Gary is young.[(triple7)] @1: Fiona is quiet.[(((triple3) -> rule1))] Gary is big.[(((triple7) -> rule2) OR ((triple6 triple4) -> rule7) OR ((triple4 ((triple5) -> rule1)) -> rule5) OR ((triple4 ((((triple4) -> rule6)) -> rule1)) -> rule5))] Gary is quiet.[(((triple5) -> rule1) OR ((((triple4) -> rule6)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple7 ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple7 ((triple4 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple7 ((triple4 ((((triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple7) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6 triple4) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple4 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple4 ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2