Charlie is round. Erin is smart. Gary is green. Harry is young. If someone is green then they are cold. Cold people are round. All young people are green.
Charlie is round.
("Charlie" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Gary is green.
True
1
proof
[(triple3)]
("Gary" "is" "green" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Gary is cold.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "green" "-")
((triple4) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Gary is round.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Gary" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
True
4
proof
[(((((((triple4) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "round" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not round.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule1)) -> rule2))]
("Harry" "is" "round" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is round.
Unknown
rconc
[@3: Erin is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Erin" "is" "round" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is round.[(triple1)] Erin is smart.[(triple2)] Gary is green.[(triple3)] Harry is young.[(triple4)] @1: Gary is cold.[(((triple3) -> rule1))] Harry is green.[(((triple4) -> rule3))] @2: Gary is round.[(((((triple3) -> rule1)) -> rule2))] Harry is cold.[(((((triple4) -> rule3)) -> rule1))] @3: Harry is round.[(((((((triple4) -> rule3)) -> rule1)) -> rule2))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple4) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3