Dave is green. Fiona is blue. Harry is young. All green people are round. All young people are green. If Dave is cold then Dave is nice. All round people are not cold. If someone is cold and not green then they are nice. If someone is young and not nice then they are blue.
Dave is green.
("Dave" "is" "green" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If Dave is cold then Dave is nice.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
All round people are not cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
If someone is cold and not green then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "nice" "+"))
If someone is young and not nice then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "blue" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Harry is green.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "green" "+")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "round" "-")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Dave" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Harry is not cold.
True
4
proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule4))]
("Harry" "is" "cold" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is cold.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule4))]
("Harry" "is" "cold" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "nice" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is green.[(triple1)] Fiona is blue.[(triple2)] Harry is young.[(triple3)] @1: Dave is round.[(((triple1) -> rule1))] Harry is green.[(((triple3) -> rule2))] @2: Dave is not cold.[(((((triple1) -> rule1)) -> rule4))] Harry is round.[(((((triple3) -> rule2)) -> rule1))] @3: Harry is not cold.[(((((((triple3) -> rule2)) -> rule1)) -> rule4))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3