Charlie is big. Erin is rough. Gary is smart. Harry is big. White people are cold. Rough, white people are nice. Green people are white. If Erin is rough then Erin is green. Green, rough people are smart. If someone is cold and not nice then they are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Rough, white people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Erin is rough then Erin is green.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "green" "+"))
Green, rough people are smart.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and not nice then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "smart" "+"))
Harry is big.
True
1
proof
[(triple4)]
("Harry" "is" "big" "+")
triple4
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Erin is green.
True
2
proof
[(((triple2) -> rule4))]
("Erin" "is" "green" "+")
((triple2) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "green" "-")
((triple2) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Erin" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Erin" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
True
4
proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule1))]
("Erin" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule3)) -> rule1))]
("Erin" "is" "cold" "-")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Charlie is big.[(triple1)] Erin is rough.[(triple2)] Gary is smart.[(triple3)] Harry is big.[(triple4)] @1: Erin is green.[(((triple2) -> rule4))] @2: Erin is smart.[(((((triple2) -> rule4) triple2) -> rule5))] Erin is white.[(((((triple2) -> rule4)) -> rule3))] @3: Erin is cold.[(((((((triple2) -> rule4)) -> rule3)) -> rule1))] Erin is nice.[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3