Erin is not big. Erin is green. Erin is smart. Gary is big. Gary is cold. Gary is not nice. Gary is rough. Gary is round. Harry is nice. Harry is rough. If Erin is smart and Erin is not rough then Erin is not green. Rough people are smart. If someone is nice and not green then they are cold. If someone is rough and not cold then they are not round. If someone is cold then they are round. If someone is smart then they are round.
Erin is not big.
("Erin" "is" "big" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Erin is smart and Erin is not rough then Erin is not green.
((("Erin" "is" "smart" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "green" "-"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice and not green then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "cold" "+"))
If someone is rough and not cold then they are not round.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "-"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple10)]
("Harry" "is" "rough" "+")
triple10
Erin is big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is round.
True
2
proof
[(((triple3) -> rule6))]
("Erin" "is" "round" "+")
((triple3) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "round" "-")
((triple3) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is round.
True
3
proof
[(((((triple10) -> rule2)) -> rule6))]
("Harry" "is" "round" "+")
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule6))]
("Harry" "is" "round" "-")
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Erin is green.[(triple2)] Erin is not big.[(triple1)] Erin is smart.[(triple3)] Gary is big.[(triple4)] Gary is cold.[(triple5)] Gary is not nice.[(triple6)] Gary is rough.[(triple7)] Gary is round.[(triple8 OR ((triple5) -> rule5) OR ((((triple7) -> rule2)) -> rule6))] Harry is nice.[(triple9)] Harry is rough.[(triple10)] @1: Erin is round.[(((triple3) -> rule6))] Gary is smart.[(((triple7) -> rule2))] Harry is smart.[(((triple10) -> rule2))] @2: Harry is round.[(((((triple10) -> rule2)) -> rule6))]
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is not big.
("Erin" "is" "big" "-")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is not nice.
("Gary" "is" "nice" "-")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
((triple5) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2