Charlie is young. Dave is blue. Dave is smart. Fiona is young. Harry is red. Harry is round. Harry is young. Round things are red. If something is smart then it is young.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Dave is young.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "young" "+")
((triple3) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "young" "-")
((triple3) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Charlie is young.[(triple1)] Dave is blue.[(triple2)] Dave is smart.[(triple3)] Fiona is young.[(triple4)] Harry is red.[(triple5 OR ((triple6) -> rule1))] Harry is round.[(triple6)] Harry is young.[(triple7)] @1: Dave is young.[(((triple3) -> rule2))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
((triple6) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1