Erin is quiet. Erin is rough. Erin is round. Fiona is rough. Gary is blue. Gary is quiet. Harry is furry. If Erin is big then Erin is quiet. If someone is smart then they are big. If Fiona is quiet then Fiona is blue. All big people are smart. Quiet people are rough. If someone is quiet and rough then they are smart.
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Erin is big then Erin is quiet.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "quiet" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Fiona is quiet then Fiona is blue.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "blue" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and rough then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Erin is quiet.
True
1
proof
[(triple1)]
("Erin" "is" "quiet" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple1)]
("Erin" "is" "quiet" "-")
triple1
Gary is rough.
True
2
proof
[(((triple6) -> rule5))]
("Gary" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple6) -> rule5))]
("Gary" "is" "rough" "-")
((triple6) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Erin is big.
True
4
proof
[(((((triple1 triple2) -> rule6)) -> rule2) OR ((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("Erin" "is" "big" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Gary is not smart.
False
4
inv-proof
[(((triple6 ((triple6) -> rule5)) -> rule6))]
("Gary" "is" "smart" "-")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is big.
True
5
proof
[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule2))]
("Gary" "is" "big" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not big.
False
5
inv-proof
[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule2))]
("Gary" "is" "big" "-")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is smart.
Unknown
rconc
[@3: Harry is smart.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule6 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "big" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Erin is quiet.[(triple1)] Erin is rough.[(triple2 OR ((triple1) -> rule5))] Erin is round.[(triple3)] Fiona is rough.[(triple4)] Gary is blue.[(triple5)] Gary is quiet.[(triple6)] Harry is furry.[(triple7)] @1: Erin is smart.[(((triple1 triple2) -> rule6) OR ((triple1 ((triple1) -> rule5)) -> rule6))] Gary is rough.[(((triple6) -> rule5))] @2: Erin is big.[(((((triple1 triple2) -> rule6)) -> rule2) OR ((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))] Gary is smart.[(((triple6 ((triple6) -> rule5)) -> rule6))] @3: Gary is big.[(((((triple6 ((triple6) -> rule5)) -> rule6)) -> rule2))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
((triple1) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple1 triple2) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((triple6 ((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple6 ((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3