Bob is cold. Fiona is green. Gary is big. Harry is cold. If something is quiet then it is young. If something is cold then it is round. Round things are young.
Bob is cold.
("Bob" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Fiona is green.
True
1
proof
[(triple2)]
("Fiona" "is" "green" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "-")
triple4
Bob is round.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "round" "+")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "round" "-")
((triple4) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("Harry" "is" "young" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is cold.[(triple1)] Fiona is green.[(triple2)] Gary is big.[(triple3)] Harry is cold.[(triple4)] @1: Bob is round.[(((triple1) -> rule2))] Harry is round.[(((triple4) -> rule2))] @2: Bob is young.[(((((triple1) -> rule2)) -> rule3))] Harry is young.[(((((triple4) -> rule2)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2